eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2015-10-12
39
0
0
10.4230/LIPIcs.TYPES.2014
article
LIPIcs, Volume 39, TYPES'14, Complete Volume
Herbelin, Hugo
Letouzey, Pierre
Sozeau, Matthieu
LIPIcs, Volume 39, TYPES'14, Complete Volume
https://drops.dagstuhl.de/storage/00lipics/lipics-vol039-types2014/LIPIcs.TYPES.2014/LIPIcs.TYPES.2014.pdf
Applicative (Functional) Programming, Software/Program Verification, Specifying and Verifying and Reasoning about Programs, Mathematical Logic
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2015-10-12
39
i
x
10.4230/LIPIcs.TYPES.2014.i
article
Front Matter, Table of Contents, Preface, Authors Index
Herbelin, Hugo
Letouzey, Pierre
Sozeau, Matthieu
Front Matter, Table of Contents, Preface, Authors Index
https://drops.dagstuhl.de/storage/00lipics/lipics-vol039-types2014/LIPIcs.TYPES.2014.i/LIPIcs.TYPES.2014.i.pdf
Front Matter
Table of Contents
Preface
Authors Index
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2015-10-12
39
1
26
10.4230/LIPIcs.TYPES.2014.1
article
Terminal Semantics for Codata Types in Intensional Martin-Löf Type Theory
Ahrens, Benedikt
Spadotti, Régis
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol039-types2014/LIPIcs.TYPES.2014.1/LIPIcs.TYPES.2014.1.pdf
relative comonad
Martin-Löf type theory
coinductive type
computer theorem proving
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2015-10-12
39
27
46
10.4230/LIPIcs.TYPES.2014.27
article
A Calculus of Constructions with Explicit Subtyping
Assaf, Ali
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol039-types2014/LIPIcs.TYPES.2014.27/LIPIcs.TYPES.2014.27.pdf
type theory
calculus of constructions
universes
cumulativity
subtyping
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2015-10-12
39
47
71
10.4230/LIPIcs.TYPES.2014.47
article
Objects and Subtyping in the Lambda-Pi-Calculus Modulo
Cauderlier, Raphaël
Dubois, Catherine
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol039-types2014/LIPIcs.TYPES.2014.47/LIPIcs.TYPES.2014.47.pdf
object
calculus
encoding
dependent type
rewrite system
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2015-10-12
39
72
88
10.4230/LIPIcs.TYPES.2014.72
article
Typeful Normalization by Evaluation
Danvy, Olivier
Keller, Chantal
Puech, Matthias
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol039-types2014/LIPIcs.TYPES.2014.72/LIPIcs.TYPES.2014.72.pdf
Normalization by Evaluation
Generalized Algebraic Data Types
Continuation-Passing Style
partial evaluation
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2015-10-12
39
89
110
10.4230/LIPIcs.TYPES.2014.89
article
Dialectica Categories and Games with Bidding
Hedges, Jules
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol039-types2014/LIPIcs.TYPES.2014.89/LIPIcs.TYPES.2014.89.pdf
Linear logic
Dialectica categories
categorical semantics
model theory
game semantics
dependent types
functional interpretations
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2015-10-12
39
111
145
10.4230/LIPIcs.TYPES.2014.111
article
The General Universal Property of the Propositional Truncation
Kraus, Nicolai
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol039-types2014/LIPIcs.TYPES.2014.111/LIPIcs.TYPES.2014.111.pdf
coherence conditions
propositional truncation
Reedy limits
universal property
well-behaved constancy
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2015-10-12
39
146
161
10.4230/LIPIcs.TYPES.2014.146
article
On the Structure of Classical Realizability Models of ZF
Krivine, Jean-Louis
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol039-types2014/LIPIcs.TYPES.2014.146/LIPIcs.TYPES.2014.146.pdf
lambda-calculus
Curry-Howard correspondence
set theory
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2015-10-12
39
162
186
10.4230/LIPIcs.TYPES.2014.162
article
An Extensional Kleene Realizability Semantics for the Minimalist Foundation
Maietti, Maria Emilia
Maschio, Samuele
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol039-types2014/LIPIcs.TYPES.2014.162/LIPIcs.TYPES.2014.162.pdf
Realizability
Type Theory
formal Church Thesis
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2015-10-12
39
187
201
10.4230/LIPIcs.TYPES.2014.187
article
Investigating Streamless Sets
Parmann, Erik
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol039-types2014/LIPIcs.TYPES.2014.187/LIPIcs.TYPES.2014.187.pdf
Type theory
Constructive Logic
Finite Sets
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2015-10-12
39
202
220
10.4230/LIPIcs.TYPES.2014.202
article
Nominal Presentation of Cubical Sets Models of Type Theory
Pitts, Andrew M.
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol039-types2014/LIPIcs.TYPES.2014.202/LIPIcs.TYPES.2014.202.pdf
models of dependent type theory
homotopy type theory
cubical sets
nominal sets
monoids
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2015-10-12
39
221
250
10.4230/LIPIcs.TYPES.2014.221
article
Extensionality of lambda-*
Polonsky, Andrew
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol039-types2014/LIPIcs.TYPES.2014.221/LIPIcs.TYPES.2014.221.pdf
Extensionality
logical relations
type theory
lambda calculus
reflection
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2015-10-12
39
251
273
10.4230/LIPIcs.TYPES.2014.251
article
Restricted Positive Quantification Is Not Elementary
Schubert, Aleksy
Urzyczyn, Pawel
Walukiewicz-Chrzaszcz, Daria
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol039-types2014/LIPIcs.TYPES.2014.251/LIPIcs.TYPES.2014.251.pdf
constructive logic
complexity
automata theory
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2015-10-12
39
274
287
10.4230/LIPIcs.TYPES.2014.274
article
On Isomorphism of Dependent Products in a Typed Logical Framework
Soloviev, Sergei
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol039-types2014/LIPIcs.TYPES.2014.274/LIPIcs.TYPES.2014.274.pdf
Isomorphism of types
dependent product
logical framework
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2015-10-12
39
288
307
10.4230/LIPIcs.TYPES.2014.288
article
An Intuitionistic Analysis of Size-change Termination
Steila, Silvia
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol039-types2014/LIPIcs.TYPES.2014.288/LIPIcs.TYPES.2014.288.pdf
Intuitionism
Ramsey's Theorem
Termination