LIPIcs, Volume 69

21st International Conference on Types for Proofs and Programs (TYPES 2015)



Thumbnail PDF

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

Documents

No documents found matching your filter selection.
Document
Complete Volume
LIPIcs, Volume 69, TYPES'15, Complete Volume

Authors: Tarmo Uustalu


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

Authors: Tarmo Uustalu


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

Authors: Robin Adams and Bart Jacobs


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

Authors: Benedikt Ahrens and Ralph Matthes


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

Authors: Thorsten Altenkirch and Ambrus Kaposi


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

Authors: Davide Ancona, Paola Giannini, and Elena Zucca


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

Authors: Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg


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

Authors: Juan Edi, Andrés Viso, and Eduardo Bonelli


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

Authors: Luca Paolini, Mauro Piccolo, and Luca Roversi


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

Authors: Erik Parmann


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

Authors: João Paulo Pizani Flor, Wouter Swierstra, and Yorick Sijsling


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}
}

Filters


Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail