Volume
LIPIcs, Volume 69
21st International Conference on Types for Proofs and Programs (TYPES 2015)
Event
TYPES 2015, May 18-21, 2015, Tallinn, EstoniaEditor
Publication Details
- published at: 2018-03-15
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-030-9
- DBLP: db/conf/types/types2015
Access Numbers
- Detailed Access Statistics available here
-
Total Document Accesses (updated on a weekly basis):
0PDF Downloads
Documents
No documents found matching your filter selection.
Document
Complete Volume
LIPIcs, Volume 69, TYPES'15, Complete Volume
Abstract
LIPIcs, Volume 69, TYPES'15, Complete Volume
Cite as
21st International Conference on Types for Proofs and Programs (TYPES 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 69, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@Proceedings{uustalu:LIPIcs.TYPES.2015,
title = {{LIPIcs, Volume 69, TYPES'15, Complete Volume}},
booktitle = {21st International Conference on Types for Proofs and Programs (TYPES 2015)},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-030-9},
ISSN = {1868-8969},
year = {2018},
volume = {69},
editor = {Uustalu, Tarmo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2015},
URN = {urn:nbn:de:0030-drops-86220},
doi = {10.4230/LIPIcs.TYPES.2015},
annote = {Keywords: Mathematical Logic and Formal Languages: Mathematical Logic - Lambda calculus and related systems}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, External Reviewers
Abstract
Front Matter, Table of Contents, Preface, External Reviewers
Cite as
21st International Conference on Types for Proofs and Programs (TYPES 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 69, pp. 0:i-0:xii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{uustalu:LIPIcs.TYPES.2015.0,
author = {Uustalu, Tarmo},
title = {{Front Matter, Table of Contents, Preface, External Reviewers}},
booktitle = {21st International Conference on Types for Proofs and Programs (TYPES 2015)},
pages = {0:i--0:xii},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-030-9},
ISSN = {1868-8969},
year = {2018},
volume = {69},
editor = {Uustalu, Tarmo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2015.0},
URN = {urn:nbn:de:0030-drops-84704},
doi = {10.4230/LIPIcs.TYPES.2015.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, External Reviewers}
}
Document
A Type Theory for Probabilistic and Bayesian Reasoning
Abstract
This paper introduces a novel type theory and logic for probabilistic reasoning. Its logic is quantitative, with fuzzy predicates. It includes normalisation and conditioning of states. This conditioning uses a key aspect that distinguishes our probabilistic type theory from quantum type theory, namely the bijective correspondence between predicates and side-effect free actions (called instrument, or assert, maps). The paper shows how suitable computation rules can be derived from this predicate-action correspondence, and uses these rules for calculating conditional probabilities in two well-known examples of Bayesian reasoning in (graphical) models. Our type theory may thus form the basis for a mechanisation of Bayesian inference.
Cite as
Robin Adams and Bart Jacobs. A Type Theory for Probabilistic and Bayesian Reasoning. In 21st International Conference on Types for Proofs and Programs (TYPES 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 69, pp. 1:1-1:34, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{adams_et_al:LIPIcs.TYPES.2015.1,
author = {Adams, Robin and Jacobs, Bart},
title = {{A Type Theory for Probabilistic and Bayesian Reasoning}},
booktitle = {21st International Conference on Types for Proofs and Programs (TYPES 2015)},
pages = {1:1--1:34},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-030-9},
ISSN = {1868-8969},
year = {2018},
volume = {69},
editor = {Uustalu, Tarmo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2015.1},
URN = {urn:nbn:de:0030-drops-84714},
doi = {10.4230/LIPIcs.TYPES.2015.1},
annote = {Keywords: Probabilistic programming, probabilistic algorithm, type theory, effect module, Bayesian reasoning}
}
Document
Heterogeneous Substitution Systems Revisited
Abstract
Matthes and Uustalu (TCS 327(1--2):155--174, 2004) presented a
categorical description of substitution systems capable of capturing
syntax involving binding which is independent of whether the syntax
is made up from least or greatest fixed points.
We extend this work
in two directions: we continue the analysis by creating more
categorical structure, in particular by organizing substitution
systems into a category and studying its properties, and we develop
the proofs of the results of the cited paper and our new ones in
UniMath, a recent library of univalent mathematics formalized in the Coq theorem
prover.
Cite as
Benedikt Ahrens and Ralph Matthes. Heterogeneous Substitution Systems Revisited. In 21st International Conference on Types for Proofs and Programs (TYPES 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 69, pp. 2:1-2:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{ahrens_et_al:LIPIcs.TYPES.2015.2,
author = {Ahrens, Benedikt and Matthes, Ralph},
title = {{Heterogeneous Substitution Systems Revisited}},
booktitle = {21st International Conference on Types for Proofs and Programs (TYPES 2015)},
pages = {2:1--2:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-030-9},
ISSN = {1868-8969},
year = {2018},
volume = {69},
editor = {Uustalu, Tarmo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2015.2},
URN = {urn:nbn:de:0030-drops-84724},
doi = {10.4230/LIPIcs.TYPES.2015.2},
annote = {Keywords: formalization of category theory, nested datatypes, Mendler-style recursion schemes, representation of substitution in languages with variable binding}
}
Document
Towards a Cubical Type Theory without an Interval
Abstract
Following the cubical set model of type theory which validates the
univalence axiom, cubical type theories have been developed that
interpret the identity type using an interval pretype. These theories start from a geometric view of equality. A proof of equality is encoded as a term in a context extended by the interval pretype. Our goal is to develop a cubical theory where the identity type is defined recursively over the type structure, and the geometry arises from these definitions. In this theory, cubes are present explicitly, e.g., a line is a telescope with 3 elements: two endpoints and the connecting equality. This is in line with Bernardy and Moulin's earlier work on internal parametricity. In this paper we present a naive syntax for internal parametricity and by replacing the parametric interpretation of the universe, we extend it to univalence. However, we do not know how to compute in this theory. As a second step, we present a version of the theory for parametricity with named dimensions which has an operational semantics. Extending this syntax to univalence is left as further work.
Cite as
Thorsten Altenkirch and Ambrus Kaposi. Towards a Cubical Type Theory without an Interval. In 21st International Conference on Types for Proofs and Programs (TYPES 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 69, pp. 3:1-3:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{altenkirch_et_al:LIPIcs.TYPES.2015.3,
author = {Altenkirch, Thorsten and Kaposi, Ambrus},
title = {{Towards a Cubical Type Theory without an Interval}},
booktitle = {21st International Conference on Types for Proofs and Programs (TYPES 2015)},
pages = {3:1--3:27},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-030-9},
ISSN = {1868-8969},
year = {2018},
volume = {69},
editor = {Uustalu, Tarmo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2015.3},
URN = {urn:nbn:de:0030-drops-84739},
doi = {10.4230/LIPIcs.TYPES.2015.3},
annote = {Keywords: homotopy type theory, parametricity, univalence}
}
Document
Constrained Polymorphic Types for a Calculus with Name Variables
Abstract
We extend the simply-typed lambda-calculus with a mechanism for dynamic rebinding of code based on parametric nominal interfaces. That is, we introduce values which represent single fragments, or families of named fragments, of open code, where free variables are associated with names which do not obey \alpha-equivalence. In this way, code fragments can be passed as function arguments and manipulated, through their nominal interface, by operators such as rebinding, overriding and renaming. Moreover, by using name variables, it is possible to write terms which are parametric in their nominal interface and/or in the way it is adapted, greatly enhancing expressivity. However, in order to prevent conflicts when instantiating name variables, the name-polymorphic types of such terms need to be equipped with simple {inequality} constraints. We show soundness of the type system.
Cite as
Davide Ancona, Paola Giannini, and Elena Zucca. Constrained Polymorphic Types for a Calculus with Name Variables. In 21st International Conference on Types for Proofs and Programs (TYPES 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 69, pp. 4:1-4:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{ancona_et_al:LIPIcs.TYPES.2015.4,
author = {Ancona, Davide and Giannini, Paola and Zucca, Elena},
title = {{Constrained Polymorphic Types for a Calculus with Name Variables}},
booktitle = {21st International Conference on Types for Proofs and Programs (TYPES 2015)},
pages = {4:1--4:29},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-030-9},
ISSN = {1868-8969},
year = {2018},
volume = {69},
editor = {Uustalu, Tarmo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2015.4},
URN = {urn:nbn:de:0030-drops-84744},
doi = {10.4230/LIPIcs.TYPES.2015.4},
annote = {Keywords: open code, incremental rebinding, name polymorphism, metaprogramming}
}
Document
Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom
Abstract
This paper presents a type theory in which it is possible to
directly manipulate $n$-dimensional cubes (points, lines, squares,
cubes, etc.) based on an interpretation of dependent type theory in
a cubical set model. This enables new ways to reason about identity
types, for instance, function extensionality is directly provable in
the system. Further, Voevodsky's univalence axiom is provable in
this system. We also explain an extension with some higher inductive
types like the circle and propositional truncation. Finally we
provide semantics for this cubical type theory in a constructive
meta-theory.
Cite as
Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. In 21st International Conference on Types for Proofs and Programs (TYPES 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 69, pp. 5:1-5:34, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{cohen_et_al:LIPIcs.TYPES.2015.5,
author = {Cohen, Cyril and Coquand, Thierry and Huber, Simon and M\"{o}rtberg, Anders},
title = {{Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom}},
booktitle = {21st International Conference on Types for Proofs and Programs (TYPES 2015)},
pages = {5:1--5:34},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-030-9},
ISSN = {1868-8969},
year = {2018},
volume = {69},
editor = {Uustalu, Tarmo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2015.5},
URN = {urn:nbn:de:0030-drops-84754},
doi = {10.4230/LIPIcs.TYPES.2015.5},
annote = {Keywords: univalence axiom, dependent type theory, cubical sets}
}
Document
Efficient Type Checking for Path Polymorphism
Abstract
A type system combining type application, constants as types, union types (associative, commutative and idempotent) and recursive types has recently been proposed for statically typing path polymorphism, the ability to define functions that can operate uniformly over
recursively specified applicative data structures. A typical pattern such functions resort to is \dataterm{x}{y} which decomposes a compound, in other words any applicative tree structure, into its parts. We study type-checking for this type system in two stages. First we propose algorithms for checking type equivalence and subtyping based on coinductive characterizations of those relations. We then formulate a syntax-directed presentation and prove its equivalence with the original one. This yields a type-checking algorithm which unfortunately has exponential time complexity in the worst case. A second algorithm is then proposed, based on automata techniques, which yields a polynomial-time type-checking algorithm.
Cite as
Juan Edi, Andrés Viso, and Eduardo Bonelli. Efficient Type Checking for Path Polymorphism. In 21st International Conference on Types for Proofs and Programs (TYPES 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 69, pp. 6:1-6:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{edi_et_al:LIPIcs.TYPES.2015.6,
author = {Edi, Juan and Viso, Andr\'{e}s and Bonelli, Eduardo},
title = {{Efficient Type Checking for Path Polymorphism}},
booktitle = {21st International Conference on Types for Proofs and Programs (TYPES 2015)},
pages = {6:1--6:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-030-9},
ISSN = {1868-8969},
year = {2018},
volume = {69},
editor = {Uustalu, Tarmo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2015.6},
URN = {urn:nbn:de:0030-drops-84761},
doi = {10.4230/LIPIcs.TYPES.2015.6},
annote = {Keywords: lambda-calculus, pattern matching, path polymorphism, type checking}
}
Document
A Certified Study of a Reversible Programming Language
Abstract
We advance in the study of the semantics of Janus, a C-like reversible programming language. Our study makes utterly explicit some backward and forward evaluation symmetries. We want to deepen mathematical knowledge about the foundations and design principles of reversible computing and programming languages. We formalize a big-step operational semantics and a denotational semantics of Janus. We show a full abstraction result between the operational and denotational semantics. Last, we certify our results by means of the proof assistant Matita.
Cite as
Luca Paolini, Mauro Piccolo, and Luca Roversi. A Certified Study of a Reversible Programming Language. In 21st International Conference on Types for Proofs and Programs (TYPES 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 69, pp. 7:1-7:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{paolini_et_al:LIPIcs.TYPES.2015.7,
author = {Paolini, Luca and Piccolo, Mauro and Roversi, Luca},
title = {{A Certified Study of a Reversible Programming Language}},
booktitle = {21st International Conference on Types for Proofs and Programs (TYPES 2015)},
pages = {7:1--7:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-030-9},
ISSN = {1868-8969},
year = {2018},
volume = {69},
editor = {Uustalu, Tarmo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2015.7},
URN = {urn:nbn:de:0030-drops-84771},
doi = {10.4230/LIPIcs.TYPES.2015.7},
annote = {Keywords: reversible computing, Janus, operational semantics, bi-deterministic evaluation, categorical semantics}
}
Document
Functional Kan Simplicial Sets: Non-Constructivity of Exponentiation
Abstract
Functional Kan simplicial sets are simplicial sets in which the horn-fillers required by the Kan extension condition are given explicitly by functions. We show the non-constructivity of the following basic result: if B and A are functional Kan simplicial sets, then A^B is a Kan simplicial set. This strengthens a similar result for the case of non-functional Kan simplicial sets shown by Bezem, Coquand and Parmann [TLCA 2015, v. 38 of LIPIcs]. Our
result shows that-from a constructive point of view-functional
Kan simplicial sets are, as it stands, unsatisfactory as a model of even simply typed lambda calculus. Our proof is based on a rather involved Kripke countermodel which has been encoded and verified in the Coq proof assistant.
Cite as
Erik Parmann. Functional Kan Simplicial Sets: Non-Constructivity of Exponentiation. In 21st International Conference on Types for Proofs and Programs (TYPES 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 69, pp. 8:1-8:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{parmann:LIPIcs.TYPES.2015.8,
author = {Parmann, Erik},
title = {{Functional Kan Simplicial Sets: Non-Constructivity of Exponentiation}},
booktitle = {21st International Conference on Types for Proofs and Programs (TYPES 2015)},
pages = {8:1--8:25},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-030-9},
ISSN = {1868-8969},
year = {2018},
volume = {69},
editor = {Uustalu, Tarmo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2015.8},
URN = {urn:nbn:de:0030-drops-84787},
doi = {10.4230/LIPIcs.TYPES.2015.8},
annote = {Keywords: constructive logic, simplicial sets, semantics of simple types}
}
Document
Pi-Ware: Hardware Description and Verification in Agda
Abstract
There is a long tradition of modelling digital circuits using functional programming languages. This paper demonstrates that by employing dependently typed programming languages, it becomes possible to define circuit descriptions that may be simulated, tested, verified and synthesized using a single language. The resulting domain specific embedded language, Pi-Ware, makes it possible to define and verify entire families of circuits at once. We demonstrate this by defining an algebra of parallel prefix circuits, proving their correctness and further algebraic properties.
Cite as
João Paulo Pizani Flor, Wouter Swierstra, and Yorick Sijsling. Pi-Ware: Hardware Description and Verification in Agda. In 21st International Conference on Types for Proofs and Programs (TYPES 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 69, pp. 9:1-9:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{pizaniflor_et_al:LIPIcs.TYPES.2015.9,
author = {Pizani Flor, Jo\~{a}o Paulo and Swierstra, Wouter and Sijsling, Yorick},
title = {{Pi-Ware: Hardware Description and Verification in Agda}},
booktitle = {21st International Conference on Types for Proofs and Programs (TYPES 2015)},
pages = {9:1--9:27},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-030-9},
ISSN = {1868-8969},
year = {2018},
volume = {69},
editor = {Uustalu, Tarmo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2015.9},
URN = {urn:nbn:de:0030-drops-84791},
doi = {10.4230/LIPIcs.TYPES.2015.9},
annote = {Keywords: dependently typed programming, Agda, EDSL, hardware description languages, functional programming}
}