Volume
LIPIcs, Volume 38
13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)
Event
TLCA 2015, July 1-3, 2015, Warsaw, PolandEditor
Publication Details
- published at: 2015-06-15
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-939897-87-3
- DBLP: db/conf/tlca/tlca2015
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 38, TLCA'15, Complete Volume
Abstract
LIPIcs, Volume 38, TLCA'15, Complete Volume
Cite as
13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@Proceedings{altenkirch:LIPIcs.TLCA.2015,
title = {{LIPIcs, Volume 38, TLCA'15, Complete Volume}},
booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-87-3},
ISSN = {1868-8969},
year = {2015},
volume = {38},
editor = {Altenkirch, Thorsten},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015},
URN = {urn:nbn:de:0030-drops-52636},
doi = {10.4230/LIPIcs.TLCA.2015},
annote = {Keywords: Applicative (Functional) Programming, Language Classifications, Language Constructs and Features, Data Structures, Logics and Meanings of Programs Mathematical Logic and Formal Languages, Symbolic and Algebraic Manipulation, Deduction and Theorem Proving}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
This volume contains the papers of the 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015), which was held during 1-3 July 2015, in Warsaw, Poland.
Cite as
13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. i-xii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{altenkirch:LIPIcs.TLCA.2015.i,
author = {Altenkirch, Thorsten},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)},
pages = {i--xii},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-87-3},
ISSN = {1868-8969},
year = {2015},
volume = {38},
editor = {Altenkirch, Thorsten},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.i},
URN = {urn:nbn:de:0030-drops-51509},
doi = {10.4230/LIPIcs.TLCA.2015.i},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Herbrand Disjunctions, Cut Elimination and Context-Free Tree Grammars
Abstract
Recently a new connection between proof theory and formal language theory was introduced. It was shown that the operation of cut elimination for proofs in first-order predicate logic involving Pi_1-cuts corresponds to computing the language of a particular class of regular tree grammars. The present paper expands this connection to the level of Pi_2-cuts. Given a proof pi of a Sigma_1 formula with cuts only on Pi_2 formulæ, we show there is associated to pi a natural context-free tree grammar whose language is finite and yields a Herbrand disjunction for pi.
Cite as
Bahareh Afshari, Stefan Hetzl, and Graham E. Leigh. Herbrand Disjunctions, Cut Elimination and Context-Free Tree Grammars. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 1-16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{afshari_et_al:LIPIcs.TLCA.2015.1,
author = {Afshari, Bahareh and Hetzl, Stefan and Leigh, Graham E.},
title = {{Herbrand Disjunctions, Cut Elimination and Context-Free Tree Grammars}},
booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)},
pages = {1--16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-87-3},
ISSN = {1868-8969},
year = {2015},
volume = {38},
editor = {Altenkirch, Thorsten},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.1},
URN = {urn:nbn:de:0030-drops-51516},
doi = {10.4230/LIPIcs.TLCA.2015.1},
annote = {Keywords: Classical logic, Context-free grammars, Cut elimination, First-order logic, Herbrand's theorem, Proof theory}
}
Document
Non-Wellfounded Trees in Homotopy Type Theory
Abstract
We prove a conjecture about the constructibility of conductive types - in the principled form of indexed M-types - in Homotopy Type Theory. The conjecture says that in the presence of inductive types, coinductive types are derivable. Indeed, in this work, we construct coinductive types in a subsystem of Homotopy Type Theory; this subsystem is given by Intensional Martin-Löf type theory with natural numbers and Voevodsky's Univalence Axiom. Our results are mechanized in the computer proof assistant Agda.
Cite as
Benedikt Ahrens, Paolo Capriotti, and Régis Spadotti. Non-Wellfounded Trees in Homotopy Type Theory. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 17-30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{ahrens_et_al:LIPIcs.TLCA.2015.17,
author = {Ahrens, Benedikt and Capriotti, Paolo and Spadotti, R\'{e}gis},
title = {{Non-Wellfounded Trees in Homotopy Type Theory}},
booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)},
pages = {17--30},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-87-3},
ISSN = {1868-8969},
year = {2015},
volume = {38},
editor = {Altenkirch, Thorsten},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.17},
URN = {urn:nbn:de:0030-drops-51522},
doi = {10.4230/LIPIcs.TLCA.2015.17},
annote = {Keywords: Homotopy Type Theory, coinductive types, computer theorem proving, Agda}
}
Document
Conservativity of Embeddings in the lambda Pi Calculus Modulo Rewriting
Abstract
The lambda Pi calculus can be extended with rewrite rules to embed
any functional pure type system. In this paper, we show that the embedding is conservative by proving a relative form of normalization, thus justifying the use of the lambda Pi calculus modulo rewriting as a logical framework for logics based on pure type systems. This result was previously only proved under the condition that the target system is normalizing. Our approach does not depend on this condition and therefore also works when the source system is not normalizing.
Cite as
Ali Assaf. Conservativity of Embeddings in the lambda Pi Calculus Modulo Rewriting. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 31-44, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{assaf:LIPIcs.TLCA.2015.31,
author = {Assaf, Ali},
title = {{Conservativity of Embeddings in the lambda Pi Calculus Modulo Rewriting}},
booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)},
pages = {31--44},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-87-3},
ISSN = {1868-8969},
year = {2015},
volume = {38},
editor = {Altenkirch, Thorsten},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.31},
URN = {urn:nbn:de:0030-drops-51535},
doi = {10.4230/LIPIcs.TLCA.2015.31},
annote = {Keywords: lambda Pi calculus modulo rewriting, pure type systems, logical framework, normalization, conservativit}
}
Document
Models for Polymorphism over Physical Dimension
Abstract
We provide a categorical framework for models of a type theory that has special types for physical quantities. The types are indexed by the physical dimensions that they involve. Fibrations are used to organize this index structure in the models of the type theory. We develop some informative models of this type theory: firstly, a model based on group actions, which captures invariance under scaling, and secondly, a way of constructing new models using relational parametricity.
Cite as
Robert Atkey, Neil Ghani, Fredrik Nordvall Forsberg, Timothy Revell, and Sam Staton. Models for Polymorphism over Physical Dimension. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 45-59, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{atkey_et_al:LIPIcs.TLCA.2015.45,
author = {Atkey, Robert and Ghani, Neil and Nordvall Forsberg, Fredrik and Revell, Timothy and Staton, Sam},
title = {{Models for Polymorphism over Physical Dimension}},
booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)},
pages = {45--59},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-87-3},
ISSN = {1868-8969},
year = {2015},
volume = {38},
editor = {Altenkirch, Thorsten},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.45},
URN = {urn:nbn:de:0030-drops-51547},
doi = {10.4230/LIPIcs.TLCA.2015.45},
annote = {Keywords: Category Theory, Units of Measure, Dimension Types, Type Theory}
}
Document
MALL Proof Equivalence is Logspace-Complete, via Binary Decision Diagrams
Abstract
Proof equivalence in a logic is the problem of deciding whether two proofs are equivalent modulo a set of permutation of rules that reflects the commutative conversions of its cut-elimination procedure. As such, it is related to the question of proofnets: finding canonical representatives of equivalence classes of proofs that have good computational properties. It can also be seen as the word problem for the notion of free category corresponding to the logic.
It has been recently shown that proof equivalence in MLL (the multiplicative with units fragment of linear logic) is Pspace-complete, which rules out any low-complexity notion of proofnet for this particular logic.
Since it is another fragment of linear logic for which attempts to define a fully satisfactory low-complexity notion of proofnet have not been successful so far, we study proof equivalence in MALL- (multiplicative-additive without units fragment of linear logic) and discover a situation that is totally different from the MLL case. Indeed, we show that proof equivalence in MALL- corresponds(under AC_0 reductions)to equivalence of binary decision diagrams, a data structure widely used to represent and analyze Boolean functions efficiently.
We show these two equivalent problems to be Logspace-complete. If this technically leaves open the possibility for a complete solution to the question of proofnets for MALL-, the established relation with binary decision diagrams actually suggests a negative solution to this problem.
Cite as
Marc Bagnol. MALL Proof Equivalence is Logspace-Complete, via Binary Decision Diagrams. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 60-75, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{bagnol:LIPIcs.TLCA.2015.60,
author = {Bagnol, Marc},
title = {{MALL Proof Equivalence is Logspace-Complete, via Binary Decision Diagrams}},
booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)},
pages = {60--75},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-87-3},
ISSN = {1868-8969},
year = {2015},
volume = {38},
editor = {Altenkirch, Thorsten},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.60},
URN = {urn:nbn:de:0030-drops-51558},
doi = {10.4230/LIPIcs.TLCA.2015.60},
annote = {Keywords: linear logic, proof equivalence, additive connectives, proofnets, binary decision diagrams, logarithmic space, AC0 reductions}
}
Document
Mixin Composition Synthesis Based on Intersection Types
Abstract
We present a method for synthesizing compositions of mixins using type inhabitation in intersection types. First, recursively defined classes and mixins, which are functions over classes, are expressed as terms in a lambda calculus with records. Intersection types with records and record-merge are used to assign meaningful types to these terms without resorting to recursive types. Second, typed terms are translated to a repository of typed combinators. We show a relation between record types with record-merge and intersection types with constructors. This relation is used to prove soundness and partial completeness of the translation with respect to mixin composition synthesis. Furthermore, we demonstrate how a translated repository and goal type can be used as input to an existing framework for composition synthesis in bounded combinatory logic via type inhabitation. The computed result corresponds to a mixin composition typed by the goal type.
Cite as
Jan Bessai, Andrej Dudenhefner, Boris Düdder, Tzu-Chun Chen, Ugo de’Liguoro, and Jakob Rehof. Mixin Composition Synthesis Based on Intersection Types. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 76-91, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{bessai_et_al:LIPIcs.TLCA.2015.76,
author = {Bessai, Jan and Dudenhefner, Andrej and D\"{u}dder, Boris and Chen, Tzu-Chun and de’Liguoro, Ugo and Rehof, Jakob},
title = {{Mixin Composition Synthesis Based on Intersection Types}},
booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)},
pages = {76--91},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-87-3},
ISSN = {1868-8969},
year = {2015},
volume = {38},
editor = {Altenkirch, Thorsten},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.76},
URN = {urn:nbn:de:0030-drops-51563},
doi = {10.4230/LIPIcs.TLCA.2015.76},
annote = {Keywords: Record Calculus, Combinatory Logic, Type Inhabitation, Mixin, Intersection Type}
}
Document
Non-Constructivity in Kan Simplicial Sets
Abstract
We give an analysis of the non-constructivity of the following basic result: if X and Y are simplicial sets and Y has the Kan extension property, then Y^X also has the Kan extension property. By means of Kripke countermodels we show that even simple consequences of this basic result, such as edge reversal and edge composition, are not constructively provable. We also show that our unprovability argument will have to be refined if one strengthens the usual formulation of the Kan extension property to one with explicit horn-filler operations.
Cite as
Marc Bezem, Thierry Coquand, and Erik Parmann. Non-Constructivity in Kan Simplicial Sets. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 92-106, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{bezem_et_al:LIPIcs.TLCA.2015.92,
author = {Bezem, Marc and Coquand, Thierry and Parmann, Erik},
title = {{Non-Constructivity in Kan Simplicial Sets}},
booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)},
pages = {92--106},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-87-3},
ISSN = {1868-8969},
year = {2015},
volume = {38},
editor = {Altenkirch, Thorsten},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.92},
URN = {urn:nbn:de:0030-drops-51579},
doi = {10.4230/LIPIcs.TLCA.2015.92},
annote = {Keywords: Constructive logic, simplicial sets, semantics of simple types}
}
Document
Logical Relations for Coherence of Effect Subtyping
Abstract
A coercion semantics of a programming language with subtyping is typically defined on typing derivations rather than on typing judgments. To avoid semantic ambiguity, such a semantics is expected to be coherent, i.e., independent of the typing derivation for a given typing judgment. In this article we present heterogeneous, biorthogonal, step-indexed logical relations for establishing the coherence of coercion semantics of programming languages with subtyping. To illustrate the effectiveness of the proof method, we develop a proof of coherence of a type-directed, selective CPS translation from a typed call-by-value lambda calculus with delimited continuations and control-effect subtyping. The article is accompanied by a Coq formalization that relies on a novel shallow embedding of a logic for reasoning about step-indexing.
Cite as
Dariusz Biernacki and Piotr Polesiuk. Logical Relations for Coherence of Effect Subtyping. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 107-122, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{biernacki_et_al:LIPIcs.TLCA.2015.107,
author = {Biernacki, Dariusz and Polesiuk, Piotr},
title = {{Logical Relations for Coherence of Effect Subtyping}},
booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)},
pages = {107--122},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-87-3},
ISSN = {1868-8969},
year = {2015},
volume = {38},
editor = {Altenkirch, Thorsten},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.107},
URN = {urn:nbn:de:0030-drops-51580},
doi = {10.4230/LIPIcs.TLCA.2015.107},
annote = {Keywords: type system, coherence of subtyping, logical relation, control effect, continuation-passing style}
}
Document
Observability for Pair Pattern Calculi
Abstract
Inspired by the notion of solvability in the λ-calculus, we define a notion of observability for a calculus with pattern matching. We give an intersection type system for such a calculus which is based on non-idempotent types. The typing system is shown to characterize the set of terms having canonical form, which properly contains the set of observable terms, so that typability alone is not sufficient to characterize observability. However, the inhabitation problem associated with our typing system turns out to be decidable, a result which — together with typability — allows to obtain a full characterization of observability.
Cite as
Antonio Bucciarelli, Delia Kesner, and Simona Ronchi Della Rocca. Observability for Pair Pattern Calculi. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 123-137, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{bucciarelli_et_al:LIPIcs.TLCA.2015.123,
author = {Bucciarelli, Antonio and Kesner, Delia and Ronchi Della Rocca, Simona},
title = {{Observability for Pair Pattern Calculi}},
booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)},
pages = {123--137},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-87-3},
ISSN = {1868-8969},
year = {2015},
volume = {38},
editor = {Altenkirch, Thorsten},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.123},
URN = {urn:nbn:de:0030-drops-51596},
doi = {10.4230/LIPIcs.TLCA.2015.123},
annote = {Keywords: solvability, pattern calculi, intersection types, inhabitation}
}
Document
Undecidability of Equality in the Free Locally Cartesian Closed Category
Abstract
We show that a version of Martin-Löf type theory with extensional identity, a unit type N1, Sigma, Pi, and a base type is a free category with families (supporting these type formers) both in a 1- and a 2-categorical sense. It follows that the underlying category of contexts is a free locally cartesian closed category in a 2-categorical sense because of a previously proved biequivalence. We then show that equality in this category is undecidable by reducing it to the undecidability of convertibility in combinatory logic.
Cite as
Simon Castellan, Pierre Clairambault, and Peter Dybjer. Undecidability of Equality in the Free Locally Cartesian Closed Category. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 138-152, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{castellan_et_al:LIPIcs.TLCA.2015.138,
author = {Castellan, Simon and Clairambault, Pierre and Dybjer, Peter},
title = {{Undecidability of Equality in the Free Locally Cartesian Closed Category}},
booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)},
pages = {138--152},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-87-3},
ISSN = {1868-8969},
year = {2015},
volume = {38},
editor = {Altenkirch, Thorsten},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.138},
URN = {urn:nbn:de:0030-drops-51602},
doi = {10.4230/LIPIcs.TLCA.2015.138},
annote = {Keywords: Extensional type theory, locally cartesian closed categories, undecidab- ility}
}
Document
The Inconsistency of a Brouwerian Continuity Principle with the Curry–Howard Interpretation
Abstract
If all functions (N -> N) -> N are continuous then 0 = 1. We establish this in intensional (and hence also in extensional) intuitionistic dependent-type theories, with existence in the formulation of continuity expressed as a Sigma type via the Curry-Howard interpretation. But with an intuitionistic notion of anonymous existence, defined as the propositional truncation of Sigma, it is consistent that all such functions are continuous. A model is Johnstone’s topological topos. On the other hand, any of these two intuitionistic conceptions of existence give the same, consistent, notion of uniform continuity for functions (N -> 2) -> N, again valid in the topological topos. It is open whether the consistency of (uniform) continuity extends to homotopy type theory. The theorems of type theory informally proved here are also formally proved in Agda, but the development presented here is self-contained and doesn't show Agda code.
Cite as
Martín Hötzel Escardó and Chuangjie Xu. The Inconsistency of a Brouwerian Continuity Principle with the Curry–Howard Interpretation. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 153-164, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{hotzelescardo_et_al:LIPIcs.TLCA.2015.153,
author = {H\"{o}tzel Escard\'{o}, Mart{\'\i}n and Xu, Chuangjie},
title = {{The Inconsistency of a Brouwerian Continuity Principle with the Curry–Howard Interpretation}},
booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)},
pages = {153--164},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-87-3},
ISSN = {1868-8969},
year = {2015},
volume = {38},
editor = {Altenkirch, Thorsten},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.153},
URN = {urn:nbn:de:0030-drops-51618},
doi = {10.4230/LIPIcs.TLCA.2015.153},
annote = {Keywords: Dependent type, intensional Martin-L\"{o}f type theory, Curry-Howard interpretation, constructive mathematics, Brouwerian continuity axioms, anonymous exi}
}
Document
Curry-Howard for Sequent Calculus at Last!
Abstract
This paper tries to remove what seems to be the remaining stumbling blocks in the way to a full understanding of the Curry-Howard isomorphism for sequent calculus, namely the questions: What do variables in proof terms stand for? What is co-control and a co-continuation? How to define the dual of Parigot's mu-operator so that it is a co-control operator? Answering these questions leads to the interpretation that sequent calculus is a formal vector notation with first-class co-control. But this is just the "internal" interpretation, which has to be developed simultaneously with, and is justified by, an equivalent, "external" interpretation, offered by natural deduction: the sequent calculus corresponds to a bi-directional, agnostic (w.r.t. the call strategy), computational lambda-calculus. Next, the formal duality between control and co-control is studied, in the context of classical logic. The duality cannot be observed in the sequent calculus, but rather in a system unifying sequent calculus and natural deduction.
Cite as
José Espírito Santo. Curry-Howard for Sequent Calculus at Last!. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 165-179, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{espiritosanto:LIPIcs.TLCA.2015.165,
author = {Esp{\'\i}rito Santo, Jos\'{e}},
title = {{Curry-Howard for Sequent Calculus at Last!}},
booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)},
pages = {165--179},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-87-3},
ISSN = {1868-8969},
year = {2015},
volume = {38},
editor = {Altenkirch, Thorsten},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.165},
URN = {urn:nbn:de:0030-drops-51626},
doi = {10.4230/LIPIcs.TLCA.2015.165},
annote = {Keywords: co-control, co-continuation, vector notation, let-expression, formal sub- stitution, context substitution, computational lambda-calculus, classical lo}
}
Document
Dependent Types for Nominal Terms with Atom Substitutions
Abstract
Nominal terms are an extended first-order language for specifying and verifying properties of syntax with binding. Founded upon the semantics of nominal sets, the success of nominal terms with regard to systems of equational reasoning is already well established. This work first extends the untyped language of nominal terms with a notion of non-capturing atom substitution for object-level names and then proposes a dependent type system for this extended language. Both these contributions are intended to serve as a prelude to a future nominal logical framework based upon nominal equational reasoning and thus an extended example is given to demonstrate that this system is capable of encoding various other formal systems of interest.
Cite as
Elliot Fairweather, Maribel Fernández, Nora Szasz, and Alvaro Tasistro. Dependent Types for Nominal Terms with Atom Substitutions. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 180-195, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{fairweather_et_al:LIPIcs.TLCA.2015.180,
author = {Fairweather, Elliot and Fern\'{a}ndez, Maribel and Szasz, Nora and Tasistro, Alvaro},
title = {{Dependent Types for Nominal Terms with Atom Substitutions}},
booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)},
pages = {180--195},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-87-3},
ISSN = {1868-8969},
year = {2015},
volume = {38},
editor = {Altenkirch, Thorsten},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.180},
URN = {urn:nbn:de:0030-drops-51636},
doi = {10.4230/LIPIcs.TLCA.2015.180},
annote = {Keywords: alpha-equivalence, nominal term, substitution, dependent type}
}
Document
Realizability Toposes from Specifications
Abstract
We investigate a framework of Krivine realizability with I/O effects, and present a method of associating realizability models to specifications on the I/O behavior of processes, by using ad- equate interpretations of the central concepts of pole and proof-like term. This method does in particular allow to associate realizability models to computable functions.
Following recent work of Streicher and others we show how these models give rise to triposes and toposes.
Cite as
Jonas Frey. Realizability Toposes from Specifications. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 196-210, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{frey:LIPIcs.TLCA.2015.196,
author = {Frey, Jonas},
title = {{Realizability Toposes from Specifications}},
booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)},
pages = {196--210},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-87-3},
ISSN = {1868-8969},
year = {2015},
volume = {38},
editor = {Altenkirch, Thorsten},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.196},
URN = {urn:nbn:de:0030-drops-51645},
doi = {10.4230/LIPIcs.TLCA.2015.196},
annote = {Keywords: Krivine machine, classical realizability, realizability topos, bisimulation}
}
Document
Standardization of a Call-By-Value Lambda-Calculus
Abstract
We study an extension of Plotkin's call-by-value lambda-calculus by means of two commutation rules (sigma-reductions). Recently, it has been proved that this extended calculus provides elegant characterizations of many semantic properties, as for example solvability. We prove a standardization theorem for this calculus by generalizing Takahashi's approach of parallel reductions. The standardization property allows us to prove that our calculus is conservative with respect to the Plotkin's one. In particular, we show that the notion of solvability for this calculus coincides with that for Plotkin's call-by-value lambda-calculus.
Cite as
Giulio Guerrieri, Luca Paolini, and Simona Ronchi Della Rocca. Standardization of a Call-By-Value Lambda-Calculus. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 211-225, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{guerrieri_et_al:LIPIcs.TLCA.2015.211,
author = {Guerrieri, Giulio and Paolini, Luca and Ronchi Della Rocca, Simona},
title = {{Standardization of a Call-By-Value Lambda-Calculus}},
booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)},
pages = {211--225},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-87-3},
ISSN = {1868-8969},
year = {2015},
volume = {38},
editor = {Altenkirch, Thorsten},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.211},
URN = {urn:nbn:de:0030-drops-51655},
doi = {10.4230/LIPIcs.TLCA.2015.211},
annote = {Keywords: standardization,sequentialization,lambda-calculus,sigma-reduction,par- allel reduction, call-by-value, head reduction, internal reduction, solvability}
}
Document
Wild omega-Categories for the Homotopy Hypothesis in Type Theory
Abstract
In classical homotopy theory, the homotopy hypothesis asserts that the fundamental varpi-groupoid construction induces an equivalence between topological spaces and weak varpi-groupoids. In the light of Voevodsky's univalent foundations program, which puts forward an interpretation of types as topological spaces, we consider the question of transposing the homotopy hypothesis to type theory. Indeed such a transposition could stand as a new approach to specifying higher inductive types. Since the formalisation of general weak varpi-groupoids in type theory is a difficult task, we only take a first step towards this goal, which consists in exploring a shortcut through strict varpi-categories.
The first outcome is a satisfactory type-theoretic notion of strict varpi-category, which has hsets of cells in all dimensions. For this notion, defining the 'fundamental strict varpi-category' of a type seems out of reach. The second outcome is an 'incoherently strict' notion of type-theoretic varpi-category, which admits arbitrary types of cells in all dimensions. These are the 'wild' varpi-categories of the title. They allow the definition of a 'fundamental wild varpi-category' map, which leads to our (partial) homotopy hypothesis for type theory (stating an adjunction, not an equivalence).
All of our results have been formalised in the Coq proof assistant. Our formalisation makes systematic use of the machinery of coinductive types.
Cite as
André Hirschowitz, Tom Hirschowitz, and Nicolas Tabareau. Wild omega-Categories for the Homotopy Hypothesis in Type Theory. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 226-240, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{hirschowitz_et_al:LIPIcs.TLCA.2015.226,
author = {Hirschowitz, Andr\'{e} and Hirschowitz, Tom and Tabareau, Nicolas},
title = {{Wild omega-Categories for the Homotopy Hypothesis in Type Theory}},
booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)},
pages = {226--240},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-87-3},
ISSN = {1868-8969},
year = {2015},
volume = {38},
editor = {Altenkirch, Thorsten},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.226},
URN = {urn:nbn:de:0030-drops-51669},
doi = {10.4230/LIPIcs.TLCA.2015.226},
annote = {Keywords: Homotopy Type theory; Omega-categories; Coinduction; Homotopy hypothesis}
}
Document
Multivariate Amortised Resource Analysis for Term Rewrite Systems
Abstract
We study amortised resource analysis in the context of term rewrite systems. We introduce a novel amortised analysis based on the potential method. The method is represented in an inference system akin to a type system and gives rise to polynomial bounds on the innermost runtime complexity of the analysed rewrite system. The crucial feature of the inference system is the admittance of multivariate bounds in the context of arbitrary data structures in a completely uniform way. This extends our earlier univariate resource analysis of typed term rewrite systems and continues our program of applying automated amortised resource analysis to rewriting.
Cite as
Martin Hofmann and Georg Moser. Multivariate Amortised Resource Analysis for Term Rewrite Systems. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 241-256, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{hofmann_et_al:LIPIcs.TLCA.2015.241,
author = {Hofmann, Martin and Moser, Georg},
title = {{Multivariate Amortised Resource Analysis for Term Rewrite Systems}},
booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)},
pages = {241--256},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-87-3},
ISSN = {1868-8969},
year = {2015},
volume = {38},
editor = {Altenkirch, Thorsten},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.241},
URN = {urn:nbn:de:0030-drops-51675},
doi = {10.4230/LIPIcs.TLCA.2015.241},
annote = {Keywords: program analysis,amortised analysis, term rewriting,multivariate bounds}
}
Document
Termination of Dependently Typed Rewrite Rules
Abstract
Our interest is in automated termination proofs of higher-order rewrite rules in presence of dependent types modulo a theory T on base types. We first describe an original transformation to a type discipline without type dependencies which preserves non-termination. Since the user must reason on expressions of the transformed language, we then introduce an extension of the computability path ordering CPO for comparing dependently typed expressions named DCPO. Using the previous result, we show that DCPO is a well-founded order, behaving well in practice.
Cite as
Jean-Pierre Jouannaud and Jianqi Li. Termination of Dependently Typed Rewrite Rules. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 257-272, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{jouannaud_et_al:LIPIcs.TLCA.2015.257,
author = {Jouannaud, Jean-Pierre and Li, Jianqi},
title = {{Termination of Dependently Typed Rewrite Rules}},
booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)},
pages = {257--272},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-87-3},
ISSN = {1868-8969},
year = {2015},
volume = {38},
editor = {Altenkirch, Thorsten},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.257},
URN = {urn:nbn:de:0030-drops-51684},
doi = {10.4230/LIPIcs.TLCA.2015.257},
annote = {Keywords: rewriting, dependent types, strong normalization, path orderings}
}
Document
Well-Founded Recursion over Contextual Objects
Abstract
We present a core programming language that supports writing well-founded structurally recursive functions using simultaneous pattern matching on contextual LF objects and contexts. The main technical tool is a coverage checking algorithm that also generates valid recursive calls. To establish consistency, we define a call-by-value small-step semantics and prove that every well-typed program terminates using a reducibility semantics. Based on the presented methodology we have implemented a totality checker as part of the programming and proof environment Beluga where it can be used to establish that a total Beluga program corresponds to a proof.
Cite as
Brigitte Pientka and Andreas Abel. Well-Founded Recursion over Contextual Objects. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 273-287, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{pientka_et_al:LIPIcs.TLCA.2015.273,
author = {Pientka, Brigitte and Abel, Andreas},
title = {{Well-Founded Recursion over Contextual Objects}},
booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)},
pages = {273--287},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-87-3},
ISSN = {1868-8969},
year = {2015},
volume = {38},
editor = {Altenkirch, Thorsten},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.273},
URN = {urn:nbn:de:0030-drops-51699},
doi = {10.4230/LIPIcs.TLCA.2015.273},
annote = {Keywords: Type systems, Dependent Types, Logical Frameworks}
}
Document
Polynomial Time in the Parametric Lambda Calculus
Abstract
In this paper we investigate Implicit Computational Complexity via the parametric lambda calculus of Ronchi Della Rocca and Paolini. We show that a particular instantiation of the set of input values leads to a characterization of polynomial time computations in a similar way to Lafont’s Soft Linear Logic. This characterization is manifestly type-free and does not require any ad hoc extensions to the pure lambda calculus. Moreover, there is a natural extension to nondeterminism with the addition of explicit products.
Cite as
Brian F. Redmond. Polynomial Time in the Parametric Lambda Calculus. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 288-301, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{redmond:LIPIcs.TLCA.2015.288,
author = {Redmond, Brian F.},
title = {{Polynomial Time in the Parametric Lambda Calculus}},
booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)},
pages = {288--301},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-87-3},
ISSN = {1868-8969},
year = {2015},
volume = {38},
editor = {Altenkirch, Thorsten},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.288},
URN = {urn:nbn:de:0030-drops-51705},
doi = {10.4230/LIPIcs.TLCA.2015.288},
annote = {Keywords: Parametric Lambda Calculus, Polynomial Time Complexity, Combinators, Nondeterminism and Explicit Products, Implicit Computational Complexity}
}
Document
Fibrations of Tree Automata
Abstract
We propose a notion of morphisms between tree automata based on game semantics. Morphisms are winning strategies on a synchronous restriction of the linear implication between acceptance games. This leads to split indexed categories, with substitution based on a suitable notion of synchronous tree function. By restricting to tree functions issued from maps on alphabets, this gives a fibration of tree automata. We then discuss the (fibrewise) monoidal structure issued from the synchronous product of automata. We also discuss how a variant of the usual projection operation on automata leads to an existential quantification in the fibered sense. Our notion of morphism is correct (it respects language inclusion), and in a weaker sense also complete.
Cite as
Colin Riba. Fibrations of Tree Automata. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 302-316, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{riba:LIPIcs.TLCA.2015.302,
author = {Riba, Colin},
title = {{Fibrations of Tree Automata}},
booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)},
pages = {302--316},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-87-3},
ISSN = {1868-8969},
year = {2015},
volume = {38},
editor = {Altenkirch, Thorsten},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.302},
URN = {urn:nbn:de:0030-drops-51719},
doi = {10.4230/LIPIcs.TLCA.2015.302},
annote = {Keywords: Tree automata, Game semantics, Categorical logic.}
}
Document
Multi-Focusing on Extensional Rewriting with Sums
Abstract
We propose a logical justification for the rewriting-based equivalence procedure for simply-typed lambda-terms with sums of Lindley. It relies on maximally multi-focused proofs, a notion of canonical derivations introduced for linear logic. Lindley’s rewriting closely corresponds to preemptive rewriting, a technical device used in the meta-theory of maximal multi-focus.
Cite as
Gabriel Scherer. Multi-Focusing on Extensional Rewriting with Sums. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 317-331, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{scherer:LIPIcs.TLCA.2015.317,
author = {Scherer, Gabriel},
title = {{Multi-Focusing on Extensional Rewriting with Sums}},
booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)},
pages = {317--331},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-87-3},
ISSN = {1868-8969},
year = {2015},
volume = {38},
editor = {Altenkirch, Thorsten},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.317},
URN = {urn:nbn:de:0030-drops-51721},
doi = {10.4230/LIPIcs.TLCA.2015.317},
annote = {Keywords: Maximal multi-focusing, extensional sums, rewriting, natural deduction}
}
Document
A Proof-theoretic Characterization of Independence in Type Theory
Abstract
For lambda-terms constructed freely from a type signature in a type theory such as LF, there is a simple inductive subordination relation that is used to control type-formation. There is a related—but not precisely complementary—notion of independence that asserts that the inhabitants of the function space tau_1 --> tau_2 depend vacuously on their arguments. Independence has many practical reasoning applications in logical frameworks, such as pruning variable dependencies or transporting theorems and proofs between type signatures. However, independence is usually not given a formal interpretation. Instead, it is generally implemented in an ad hoc and uncertified fashion. We propose a formal definition of independence and give a proof-theoretic characterization of it by: (1) representing the inference rules of a given type theory and a closed type signature as a theory of intuitionistic predicate logic, (2) showing that typing derivations in this signature are adequately represented by a focused sequent calculus for this logic, and (3) defining independence in terms of strengthening for intuitionistic sequents. This scheme is then formalized in a meta-logic, called G, that can represent the sequent calculus as an inductive definition, so the relevant strengthening lemmas can be given explicit inductive proofs. We present an algorithm for automatically deriving the strengthening lemmas and their proofs in G.
Cite as
Yuting Wang and Kaustuv Chaudhuri. A Proof-theoretic Characterization of Independence in Type Theory. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 332-346, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{wang_et_al:LIPIcs.TLCA.2015.332,
author = {Wang, Yuting and Chaudhuri, Kaustuv},
title = {{A Proof-theoretic Characterization of Independence in Type Theory}},
booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)},
pages = {332--346},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-87-3},
ISSN = {1868-8969},
year = {2015},
volume = {38},
editor = {Altenkirch, Thorsten},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.332},
URN = {urn:nbn:de:0030-drops-51736},
doi = {10.4230/LIPIcs.TLCA.2015.332},
annote = {Keywords: subordination; independence; sequent calculus; focusing; strengthening}
}