20th International Conference on Types for Proofs and Programs (TYPES 2014)

Document

Complete Volume

DOI: 10.4230/LIPIcs.TYPES.2014

LIPIcs, Volume 39, TYPES'14, Complete Volume

Authors: Hugo Herbelin, Pierre Letouzey, and Matthieu Sozeau

Abstract

LIPIcs, Volume 39, TYPES'14, Complete Volume

Cite as

20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@Proceedings{herbelin_et_al:LIPIcs.TYPES.2014,
  title =	{{LIPIcs, Volume 39, TYPES'14, Complete Volume}},
  booktitle =	{20th International Conference on Types for Proofs and Programs (TYPES 2014)},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-88-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{39},
  editor =	{Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014},
  URN =		{urn:nbn:de:0030-drops-55047},
  doi =		{10.4230/LIPIcs.TYPES.2014},
  annote =	{Keywords: Applicative (Functional) Programming, Software/Program Verification, Specifying and Verifying and Reasoning about Programs, Mathematical Logic}
}

Document

Front Matter

DOI: 10.4230/LIPIcs.TYPES.2014.i

Front Matter, Table of Contents, Preface, Authors Index

Authors: Hugo Herbelin, Pierre Letouzey, and Matthieu Sozeau

Abstract

Front Matter, Table of Contents, Preface, Authors Index

Cite as

20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. i-x, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{herbelin_et_al:LIPIcs.TYPES.2014.i,
  author =	{Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu},
  title =	{{Front Matter, Table of Contents, Preface, Authors Index}},
  booktitle =	{20th International Conference on Types for Proofs and Programs (TYPES 2014)},
  pages =	{i--x},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-88-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{39},
  editor =	{Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014.i},
  URN =		{urn:nbn:de:0030-drops-54888},
  doi =		{10.4230/LIPIcs.TYPES.2014.i},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Authors Index}
}

Document

DOI: 10.4230/LIPIcs.TYPES.2014.1

Terminal Semantics for Codata Types in Intensional Martin-Löf Type Theory

Authors: Benedikt Ahrens and Régis Spadotti

Abstract

We study the notions of relative comonad and comodule over a relative comonad. We use these notions to give categorical semantics for the coinductive type families of streams and of infinite triangular matrices and their respective cosubstitution operations in intensional Martin-Löf type theory. Our results are mechanized in the proof assistant Coq.

Cite as

Benedikt Ahrens and Régis Spadotti. Terminal Semantics for Codata Types in Intensional Martin-Löf Type Theory. In 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. 1-26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{ahrens_et_al:LIPIcs.TYPES.2014.1,
  author =	{Ahrens, Benedikt and Spadotti, R\'{e}gis},
  title =	{{Terminal Semantics for Codata Types in Intensional Martin-L\"{o}f Type Theory}},
  booktitle =	{20th International Conference on Types for Proofs and Programs (TYPES 2014)},
  pages =	{1--26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-88-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{39},
  editor =	{Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014.1},
  URN =		{urn:nbn:de:0030-drops-54891},
  doi =		{10.4230/LIPIcs.TYPES.2014.1},
  annote =	{Keywords: relative comonad, Martin-L\"{o}f type theory, coinductive type, computer theorem proving}
}

Document

DOI: 10.4230/LIPIcs.TYPES.2014.27

A Calculus of Constructions with Explicit Subtyping

Authors: Ali Assaf

Abstract

The calculus of constructions can be extended with an infinite hierarchy of universes and cumulative subtyping. Subtyping is usually left implicit in the typing rules. We present an alternative version of the calculus of constructions where subtyping is explicit. We avoid problems related to coercions and dependent types by using the Tarski style of universes and by adding equations to reflect equality.

Cite as

Ali Assaf. A Calculus of Constructions with Explicit Subtyping. In 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. 27-46, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{assaf:LIPIcs.TYPES.2014.27,
  author =	{Assaf, Ali},
  title =	{{A Calculus of Constructions with Explicit Subtyping}},
  booktitle =	{20th International Conference on Types for Proofs and Programs (TYPES 2014)},
  pages =	{27--46},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-88-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{39},
  editor =	{Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014.27},
  URN =		{urn:nbn:de:0030-drops-54904},
  doi =		{10.4230/LIPIcs.TYPES.2014.27},
  annote =	{Keywords: type theory, calculus of constructions, universes, cumulativity, subtyping}
}

Document

DOI: 10.4230/LIPIcs.TYPES.2014.47

Objects and Subtyping in the Lambda-Pi-Calculus Modulo

Authors: Raphaël Cauderlier and Catherine Dubois

Abstract

We present a shallow embedding of the Object Calculus of Abadi and Cardelli in the lambda-Pi-calculus modulo, an extension of the lambda-Pi-calculus with rewriting. This embedding may be used as an example of translation of subtyping. We prove this embedding correct with respect to the operational semantics and the type system of the Object Calculus. We implemented a translation tool from the Object Calculus to Dedukti, a type-checker for the lambda-Pi-calculus modulo.

Cite as

Raphaël Cauderlier and Catherine Dubois. Objects and Subtyping in the Lambda-Pi-Calculus Modulo. In 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. 47-71, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{cauderlier_et_al:LIPIcs.TYPES.2014.47,
  author =	{Cauderlier, Rapha\"{e}l and Dubois, Catherine},
  title =	{{Objects and Subtyping in the Lambda-Pi-Calculus Modulo}},
  booktitle =	{20th International Conference on Types for Proofs and Programs (TYPES 2014)},
  pages =	{47--71},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-88-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{39},
  editor =	{Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014.47},
  URN =		{urn:nbn:de:0030-drops-54919},
  doi =		{10.4230/LIPIcs.TYPES.2014.47},
  annote =	{Keywords: object, calculus, encoding, dependent type, rewrite system}
}

Document

DOI: 10.4230/LIPIcs.TYPES.2014.72

Typeful Normalization by Evaluation

Authors: Olivier Danvy, Chantal Keller, and Matthias Puech

Abstract

We present the first typeful implementation of Normalization by Evaluation for the simply typed lambda-calculus with sums and control operators: we guarantee type preservation and eta-long (modulo commuting conversions), beta-normal forms using only Generalized Algebraic Data Types in a general-purpose programming language, here OCaml; and we account for sums and control operators with Continuation-Passing Style. First, we implement the standard NbE algorithm for the implicational fragment in a typeful way that is correct by construction. We then derive its call-by-value continuation-passing counterpart, that maps a lambda-term with sums and call/cc into a CPS term in normal form, which we express in a typed dedicated syntax. Beyond showcasing the expressive power of GADTs, we emphasize that type inference gives a smooth way to re-derive the encodings of the syntax and typing of normal forms in Continuation-Passing Style.

Cite as

Olivier Danvy, Chantal Keller, and Matthias Puech. Typeful Normalization by Evaluation. In 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. 72-88, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{danvy_et_al:LIPIcs.TYPES.2014.72,
  author =	{Danvy, Olivier and Keller, Chantal and Puech, Matthias},
  title =	{{Typeful Normalization by Evaluation}},
  booktitle =	{20th International Conference on Types for Proofs and Programs (TYPES 2014)},
  pages =	{72--88},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-88-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{39},
  editor =	{Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014.72},
  URN =		{urn:nbn:de:0030-drops-54921},
  doi =		{10.4230/LIPIcs.TYPES.2014.72},
  annote =	{Keywords: Normalization by Evaluation, Generalized Algebraic Data Types, Continuation-Passing Style, partial evaluation}
}

Document

DOI: 10.4230/LIPIcs.TYPES.2014.89

Dialectica Categories and Games with Bidding

Authors: Jules Hedges

Abstract

This paper presents a construction which transforms categorical models of additive-free propositional linear logic, closely based on de Paiva's dialectica categories and Oliva's functional interpretations of classical linear logic. The construction is defined using dependent type theory, which proves to be a useful tool for reasoning about dialectica categories. Abstractly, we have a closure operator on the class of models: it preserves soundness and completeness and has a monad-like structure. When applied to categories of games we obtain 'games with bidding', which are hybrids of dialectica and game models, and we prove completeness theorems for two specific such models.

Cite as

Jules Hedges. Dialectica Categories and Games with Bidding. In 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. 89-110, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{hedges:LIPIcs.TYPES.2014.89,
  author =	{Hedges, Jules},
  title =	{{Dialectica Categories and Games with Bidding}},
  booktitle =	{20th International Conference on Types for Proofs and Programs (TYPES 2014)},
  pages =	{89--110},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-88-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{39},
  editor =	{Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014.89},
  URN =		{urn:nbn:de:0030-drops-54937},
  doi =		{10.4230/LIPIcs.TYPES.2014.89},
  annote =	{Keywords: Linear logic, Dialectica categories, categorical semantics, model theory, game semantics, dependent types, functional interpretations}
}

Document

DOI: 10.4230/LIPIcs.TYPES.2014.111

The General Universal Property of the Propositional Truncation

Authors: Nicolai Kraus

Abstract

In a type-theoretic fibration category in the sense of Shulman (representing a dependent type theory with at least unit, sigma, pi, and identity types), we define the type of coherently constant functions from A to B. This involves an infinite tower of coherence conditions, and we therefore need the category to have Reedy limits of diagrams over omega^op. Our main result is that, if the category further has propositional truncations and satisfies function extensionality, the type of coherently constant function is equivalent to the type ||A|| -> B. If B is an n-type for a given finite n, the tower of coherence conditions becomes finite and the requirement of nontrivial Reedy limits vanishes. The whole construction can then be carried out in standard syntactical homotopy type theory and generalises the universal property of the truncation. This provides a way to define functions ||A|| -> B if B is not known to be propositional, and it streamlines the common approach of finding a propositional type Q with A -> Q and Q -> B.

Cite as

Nicolai Kraus. The General Universal Property of the Propositional Truncation. In 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. 111-145, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{kraus:LIPIcs.TYPES.2014.111,
  author =	{Kraus, Nicolai},
  title =	{{The General Universal Property of the Propositional Truncation}},
  booktitle =	{20th International Conference on Types for Proofs and Programs (TYPES 2014)},
  pages =	{111--145},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-88-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{39},
  editor =	{Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014.111},
  URN =		{urn:nbn:de:0030-drops-54944},
  doi =		{10.4230/LIPIcs.TYPES.2014.111},
  annote =	{Keywords: coherence conditions, propositional truncation, Reedy limits, universal property, well-behaved constancy}
}

Document

DOI: 10.4230/LIPIcs.TYPES.2014.146

On the Structure of Classical Realizability Models of ZF

Authors: Jean-Louis Krivine

Abstract

The technique of classical realizability is an extension of the method of forcing; it permits to extend the Curry-Howard correspondence between proofs and programs, to Zermelo-Fraenkel set theory and to build new models of ZF, called realizability models. The structure of these models is, in general, much more complicated than that of the particular case of forcing models. We show here that the class of constructible sets of any realizability model is an elementary extension of the constructibles of the ground model (a trivial fact in the case of forcing, since these classes are identical). By Shoenfield absoluteness theorem, it follows that every true Sigma^1_3 formula is realized by a closed lambda_c-term.

Cite as

Jean-Louis Krivine. On the Structure of Classical Realizability Models of ZF. In 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. 146-161, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{krivine:LIPIcs.TYPES.2014.146,
  author =	{Krivine, Jean-Louis},
  title =	{{On the Structure of Classical Realizability Models of ZF}},
  booktitle =	{20th International Conference on Types for Proofs and Programs (TYPES 2014)},
  pages =	{146--161},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-88-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{39},
  editor =	{Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014.146},
  URN =		{urn:nbn:de:0030-drops-54953},
  doi =		{10.4230/LIPIcs.TYPES.2014.146},
  annote =	{Keywords: lambda-calculus, Curry-Howard correspondence, set theory}
}

Document

DOI: 10.4230/LIPIcs.TYPES.2014.162

An Extensional Kleene Realizability Semantics for the Minimalist Foundation

Authors: Maria Emilia Maietti and Samuele Maschio

Abstract

We build a Kleene realizability semantics for the two-level Minimalist Foundation MF, ideated by Maietti and Sambin in 2005 and completed by Maietti in 2009. Thanks to this semantics we prove that both levels of MF are consistent with the formal Church Thesis CT. Since MF consists of two levels, an intensional one, called mtt, and an extensional one, called emtt, linked by an interpretation, it is enough to build a realizability semantics for the intensional level mtt to get one for the extensional one emtt, too. Moreover, both levels consists of type theories based on versions of Martin-Löf's type theory. Our realizability semantics for mtt is a modification of the realizability semantics by Beeson in 1985 for extensional first order Martin-Löf's type theory with one universe. So it is formalized in Feferman's classical arithmetic theory of inductive definitions, called ID1^. It is called extensional Kleene realizability semantics since it validates extensional equality of type-theoretic functions extFun, as in Beeson's one. The main modification we perform on Beeson's semantics is to interpret propositions, which are defined primitively in MF, in a proof-irrelevant way. As a consequence, we gain the validity of CT. Recalling that extFun+CT+AC are inconsistent over arithmetics with finite types, we conclude that our semantics does not validate the Axiom of Choice AC on generic types. On the contrary, Beeson's semantics does validate AC, being this a theorem of Martin-Löf's theory, but it does not validate CT. The semantics we present here seems to be the best approximation of Kleene realizability for the extensional level emtt. Indeed Beeson's semantics is not an option for emtt since AC on generic sets added to it entails the excluded middle.

Cite as

Maria Emilia Maietti and Samuele Maschio. An Extensional Kleene Realizability Semantics for the Minimalist Foundation. In 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. 162-186, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{maietti_et_al:LIPIcs.TYPES.2014.162,
  author =	{Maietti, Maria Emilia and Maschio, Samuele},
  title =	{{An Extensional Kleene Realizability Semantics for the Minimalist Foundation}},
  booktitle =	{20th International Conference on Types for Proofs and Programs (TYPES 2014)},
  pages =	{162--186},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-88-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{39},
  editor =	{Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014.162},
  URN =		{urn:nbn:de:0030-drops-54966},
  doi =		{10.4230/LIPIcs.TYPES.2014.162},
  annote =	{Keywords: Realizability, Type Theory, formal Church Thesis}
}

Document

DOI: 10.4230/LIPIcs.TYPES.2014.187

Investigating Streamless Sets

Authors: Erik Parmann

Abstract

In this paper we look at streamless sets, recently investigated by Coquand and Spiwack. A set is streamless if every stream over that set contain a duplicate. It is an open question in constructive mathematics whether the Cartesian product of two streamless sets is streamless. We look at some settings in which the Cartesian product of two streamless sets is indeed streamless; in particular, we show that this holds in Martin-Loef intentional type theory when at least one of the sets have decidable equality. We go on to show that the addition of functional extensionality give streamless sets decidable equality, and then investigate these results in a few other constructive systems.

Cite as

Erik Parmann. Investigating Streamless Sets. In 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. 187-201, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{parmann:LIPIcs.TYPES.2014.187,
  author =	{Parmann, Erik},
  title =	{{Investigating Streamless Sets}},
  booktitle =	{20th International Conference on Types for Proofs and Programs (TYPES 2014)},
  pages =	{187--201},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-88-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{39},
  editor =	{Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014.187},
  URN =		{urn:nbn:de:0030-drops-54971},
  doi =		{10.4230/LIPIcs.TYPES.2014.187},
  annote =	{Keywords: Type theory, Constructive Logic, Finite Sets}
}

Document

DOI: 10.4230/LIPIcs.TYPES.2014.202

Nominal Presentation of Cubical Sets Models of Type Theory

Authors: Andrew M. Pitts

Abstract

The cubical sets model of Homotopy Type Theory introduced by Bezem, Coquand and Huber uses a particular category of presheaves. We show that this presheaf category is equivalent to a category of sets equipped with an action of a monoid of name substitutions for which a finite support property holds. That category is in turn isomorphic to a category of nominal sets equipped with operations for substituting constants 0 and 1 for names. This formulation of cubical sets brings out the potentially useful connection that exists between the homotopical notion of path and the nominal sets notion of name abstraction. The formulation in terms of actions of monoids of name substitutions also encompasses a variant category of cubical sets with diagonals, equivalent to presheaves on Grothendieck's "smallest test category." We show that this category has the pleasant property that path objects given by name abstraction are exponentials with respect to an interval object.

Cite as

Andrew M. Pitts. Nominal Presentation of Cubical Sets Models of Type Theory. In 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. 202-220, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{pitts:LIPIcs.TYPES.2014.202,
  author =	{Pitts, Andrew M.},
  title =	{{Nominal Presentation of Cubical Sets Models of Type Theory}},
  booktitle =	{20th International Conference on Types for Proofs and Programs (TYPES 2014)},
  pages =	{202--220},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-88-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{39},
  editor =	{Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014.202},
  URN =		{urn:nbn:de:0030-drops-54980},
  doi =		{10.4230/LIPIcs.TYPES.2014.202},
  annote =	{Keywords: models of dependent type theory, homotopy type theory, cubical sets, nominal sets, monoids}
}

Document

DOI: 10.4230/LIPIcs.TYPES.2014.221

Extensionality of lambda-*

Authors: Andrew Polonsky

Abstract

We prove an extensionality theorem for the "type-in-type" dependent type theory with Sigma-types. We suggest that in type theory the notion of extensional equality be identified with the logical equivalence relation defined by induction on type structure.

Cite as

Andrew Polonsky. Extensionality of lambda-*. In 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. 221-250, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{polonsky:LIPIcs.TYPES.2014.221,
  author =	{Polonsky, Andrew},
  title =	{{Extensionality of lambda-*}},
  booktitle =	{20th International Conference on Types for Proofs and Programs (TYPES 2014)},
  pages =	{221--250},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-88-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{39},
  editor =	{Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014.221},
  URN =		{urn:nbn:de:0030-drops-54995},
  doi =		{10.4230/LIPIcs.TYPES.2014.221},
  annote =	{Keywords: Extensionality, logical relations, type theory, lambda calculus, reflection}
}

Document

DOI: 10.4230/LIPIcs.TYPES.2014.251

Restricted Positive Quantification Is Not Elementary

Authors: Aleksy Schubert, Pawel Urzyczyn, and Daria Walukiewicz-Chrzaszcz

Abstract

We show that a restricted variant of constructive predicate logic with positive (covariant) quantification is of super-elementary complexity. The restriction is to limit the number of eigenvariables used in quantifier introductions rules to a reasonably usable level. This construction suggests that the known non-elementary decision algorithms for positive logic may actually be best possible.

Cite as

Aleksy Schubert, Pawel Urzyczyn, and Daria Walukiewicz-Chrzaszcz. Restricted Positive Quantification Is Not Elementary. In 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. 251-273, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{schubert_et_al:LIPIcs.TYPES.2014.251,
  author =	{Schubert, Aleksy and Urzyczyn, Pawel and Walukiewicz-Chrzaszcz, Daria},
  title =	{{Restricted Positive Quantification Is Not Elementary}},
  booktitle =	{20th International Conference on Types for Proofs and Programs (TYPES 2014)},
  pages =	{251--273},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-88-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{39},
  editor =	{Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014.251},
  URN =		{urn:nbn:de:0030-drops-55002},
  doi =		{10.4230/LIPIcs.TYPES.2014.251},
  annote =	{Keywords: constructive logic, complexity, automata theory}
}

Document

DOI: 10.4230/LIPIcs.TYPES.2014.274

On Isomorphism of Dependent Products in a Typed Logical Framework

Authors: Sergei Soloviev

Abstract

A complete decision procedure for isomorphism of kinds that contain only dependent product, constant Type and variables is obtained. All proofs are done using Z. Luo's logical framework. They can be easily transferred to a large class of type theories with dependent product.

Cite as

Sergei Soloviev. On Isomorphism of Dependent Products in a Typed Logical Framework. In 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. 274-287, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{soloviev:LIPIcs.TYPES.2014.274,
  author =	{Soloviev, Sergei},
  title =	{{On Isomorphism of Dependent Products in a Typed Logical Framework}},
  booktitle =	{20th International Conference on Types for Proofs and Programs (TYPES 2014)},
  pages =	{274--287},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-88-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{39},
  editor =	{Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014.274},
  URN =		{urn:nbn:de:0030-drops-55013},
  doi =		{10.4230/LIPIcs.TYPES.2014.274},
  annote =	{Keywords: Isomorphism of types, dependent product, logical framework}
}

Document

DOI: 10.4230/LIPIcs.TYPES.2014.288

An Intuitionistic Analysis of Size-change Termination

Authors: Silvia Steila

Abstract

In 2001 Lee, Jones and Ben-Amram introduced the notion of size-change termination (SCT) for first order functional programs, a sufficient condition for termination. They proved that a program is size-change terminating if and only if it has a certain property which can be statically verified from the recursive definition of the program. Their proof of the size-change termination theorem used Ramsey's Theorem for pairs, which is a purely classical result. In 2012 Vytiniotis, Coquand and Wahlsteldt intuitionistically proved a classical variant of the size-change termination theorem by using the Almost-Full Theorem instead of Ramsey's Theorem for pairs. In this paper we provide an intuitionistic proof of another classical variant of the SCT theorem: our goal is to provide a statement and a proof very similar to the original ones. This can be done by using the H-closure Theorem, which differs from Ramsey's Theorem for pairs only by a contrapositive step. As a side result we obtain another proof of the characterization of the functions computed by a tail-recursive SCT program, by relating the SCT Theorem with the Termination Theorem by Podelski and Rybalchenko. Finally, by investigating the relationship between them, we provide a property in the "language" of size-change termination which is equivalent to Podelski and Rybalchenko's termination.

Cite as

Silvia Steila. An Intuitionistic Analysis of Size-change Termination. In 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. 288-307, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{steila:LIPIcs.TYPES.2014.288,
  author =	{Steila, Silvia},
  title =	{{An Intuitionistic Analysis of Size-change Termination}},
  booktitle =	{20th International Conference on Types for Proofs and Programs (TYPES 2014)},
  pages =	{288--307},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-88-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{39},
  editor =	{Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014.288},
  URN =		{urn:nbn:de:0030-drops-55026},
  doi =		{10.4230/LIPIcs.TYPES.2014.288},
  annote =	{Keywords: Intuitionism, Ramsey's Theorem, Termination}
}

LIPIcs, Volume 39

20th International Conference on Types for Proofs and Programs (TYPES 2014)

Event

Editors

Publication Details

Access Numbers

Documents

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Filters

Thanks for your feedback!

Could not send message