13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)

Document

Complete Volume

DOI: 10.4230/LIPIcs.TLCA.2015

LIPIcs, Volume 38, TLCA'15, Complete Volume

Authors: Thorsten Altenkirch

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

DOI: 10.4230/LIPIcs.TLCA.2015.i

Front Matter, Table of Contents, Preface, Conference Organization

Authors: Thorsten Altenkirch

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

DOI: 10.4230/LIPIcs.TLCA.2015.1

Herbrand Disjunctions, Cut Elimination and Context-Free Tree Grammars

Authors: Bahareh Afshari, Stefan Hetzl, and Graham E. Leigh

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

DOI: 10.4230/LIPIcs.TLCA.2015.17

Non-Wellfounded Trees in Homotopy Type Theory

Authors: Benedikt Ahrens, Paolo Capriotti, and Régis Spadotti

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

DOI: 10.4230/LIPIcs.TLCA.2015.31

Conservativity of Embeddings in the lambda Pi Calculus Modulo Rewriting

Authors: Ali Assaf

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

DOI: 10.4230/LIPIcs.TLCA.2015.45

Models for Polymorphism over Physical Dimension

Authors: Robert Atkey, Neil Ghani, Fredrik Nordvall Forsberg, Timothy Revell, and Sam Staton

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

DOI: 10.4230/LIPIcs.TLCA.2015.60

MALL Proof Equivalence is Logspace-Complete, via Binary Decision Diagrams

Authors: Marc Bagnol

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

DOI: 10.4230/LIPIcs.TLCA.2015.76

Mixin Composition Synthesis Based on Intersection Types

Authors: Jan Bessai, Andrej Dudenhefner, Boris Düdder, Tzu-Chun Chen, Ugo de’Liguoro, and Jakob Rehof

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

DOI: 10.4230/LIPIcs.TLCA.2015.92

Non-Constructivity in Kan Simplicial Sets

Authors: Marc Bezem, Thierry Coquand, and Erik Parmann

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

DOI: 10.4230/LIPIcs.TLCA.2015.107

Logical Relations for Coherence of Effect Subtyping

Authors: Dariusz Biernacki and Piotr Polesiuk

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

DOI: 10.4230/LIPIcs.TLCA.2015.123

Observability for Pair Pattern Calculi

Authors: Antonio Bucciarelli, Delia Kesner, and Simona Ronchi Della Rocca

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

DOI: 10.4230/LIPIcs.TLCA.2015.138

Undecidability of Equality in the Free Locally Cartesian Closed Category

Authors: Simon Castellan, Pierre Clairambault, and Peter Dybjer

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

DOI: 10.4230/LIPIcs.TLCA.2015.153

The Inconsistency of a Brouwerian Continuity Principle with the Curry–Howard Interpretation

Authors: Martín Hötzel Escardó and Chuangjie Xu

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

DOI: 10.4230/LIPIcs.TLCA.2015.165

Curry-Howard for Sequent Calculus at Last!

Authors: José Espírito Santo

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

DOI: 10.4230/LIPIcs.TLCA.2015.180

Dependent Types for Nominal Terms with Atom Substitutions

Authors: Elliot Fairweather, Maribel Fernández, Nora Szasz, and Alvaro Tasistro

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

DOI: 10.4230/LIPIcs.TLCA.2015.196

Realizability Toposes from Specifications

Authors: Jonas Frey

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

DOI: 10.4230/LIPIcs.TLCA.2015.211

Standardization of a Call-By-Value Lambda-Calculus

Authors: Giulio Guerrieri, Luca Paolini, and Simona Ronchi Della Rocca

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

DOI: 10.4230/LIPIcs.TLCA.2015.226

Wild omega-Categories for the Homotopy Hypothesis in Type Theory

Authors: André Hirschowitz, Tom Hirschowitz, and Nicolas Tabareau

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

DOI: 10.4230/LIPIcs.TLCA.2015.241

Multivariate Amortised Resource Analysis for Term Rewrite Systems

Authors: Martin Hofmann and Georg Moser

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

DOI: 10.4230/LIPIcs.TLCA.2015.257

Termination of Dependently Typed Rewrite Rules

Authors: Jean-Pierre Jouannaud and Jianqi Li

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

DOI: 10.4230/LIPIcs.TLCA.2015.273

Well-Founded Recursion over Contextual Objects

Authors: Brigitte Pientka and Andreas Abel

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

DOI: 10.4230/LIPIcs.TLCA.2015.288

Polynomial Time in the Parametric Lambda Calculus

Authors: Brian F. Redmond

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

DOI: 10.4230/LIPIcs.TLCA.2015.302

Fibrations of Tree Automata

Authors: Colin Riba

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

DOI: 10.4230/LIPIcs.TLCA.2015.317

Multi-Focusing on Extensional Rewriting with Sums

Authors: Gabriel Scherer

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

DOI: 10.4230/LIPIcs.TLCA.2015.332

A Proof-theoretic Characterization of Independence in Type Theory

Authors: Yuting Wang and Kaustuv Chaudhuri

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

LIPIcs, Volume 38

13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)

Event

Editor

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

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