Volume
LIPIcs, Volume 97
22nd International Conference on Types for Proofs and Programs (TYPES 2016)
Event
TYPES 2016, May 23-26, 2016, Novi Sad, SerbiaEditors
Publication Details
- published at: 2018-11-05
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-065-1
- DBLP: db/conf/types/types2016
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 97, TYPES'16, Complete Volume
Abstract
LIPIcs, Volume 97, TYPES'16, Complete Volume
Cite as
22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@Proceedings{ghilezan_et_al:LIPIcs.TYPES.2016,
title = {{LIPIcs, Volume 97, TYPES'16, Complete Volume}},
booktitle = {22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-065-1},
ISSN = {1868-8969},
year = {2018},
volume = {97},
editor = {Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016},
URN = {urn:nbn:de:0030-drops-98651},
doi = {10.4230/LIPIcs.TYPES.2016},
annote = {Keywords: Theory of computation, Type theory}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 0:i-0:x, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{ghilezan_et_al:LIPIcs.TYPES.2016.0,
author = {Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
pages = {0:i--0:x},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-065-1},
ISSN = {1868-8969},
year = {2018},
volume = {97},
editor = {Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.0},
URN = {urn:nbn:de:0030-drops-98466},
doi = {10.4230/LIPIcs.TYPES.2016.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Paper
Mechanized Metatheory Revisited: An Extended Abstract (Invited Paper)
Abstract
Proof assistants and the programming languages that implement them need to deal with a range of linguistic expressions that involve bindings. Since most mature proof assistants do not have built-in methods to treat this aspect of syntax, many of them have been extended with various packages and libraries that allow them to encode bindings using, for example, de Bruijn numerals and nominal logic features. I put forward the argument that bindings are such an intimate aspect of the structure of expressions that they should be accounted for directly in the underlying programming language support for proof assistants and not added later using packages and libraries. One possible approach to designing programming languages and proof assistants that directly supports such an approach to bindings in syntax is presented. The roots of such an approach can be found in the mobility of binders between term-level bindings, formula-level bindings (quantifiers), and proof-level bindings (eigenvariables). In particular, by combining Church's approach to terms and formulas (found in his Simple Theory of Types) and Gentzen's approach to sequent calculus proofs, we can learn how bindings can declaratively interact with the full range of logical connectives and quantifiers. I will also illustrate how that framework provides an intimate and semantically clean treatment of computation and reasoning with syntax containing bindings. Some implemented systems, which support this intimate and built-in treatment of bindings, will be briefly described.
Cite as
Dale Miller. Mechanized Metatheory Revisited: An Extended Abstract (Invited Paper). In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 1:1-1:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{miller:LIPIcs.TYPES.2016.1,
author = {Miller, Dale},
title = {{Mechanized Metatheory Revisited: An Extended Abstract}},
booktitle = {22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
pages = {1:1--1:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-065-1},
ISSN = {1868-8969},
year = {2018},
volume = {97},
editor = {Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.1},
URN = {urn:nbn:de:0030-drops-98603},
doi = {10.4230/LIPIcs.TYPES.2016.1},
annote = {Keywords: mechanized metatheory, mobility of binders, lambda-tree syntax, higher-order abstract syntax}
}
Document
Invited Paper
Intersection Types and Denotational Semantics: An Extended Abstract (Invited Paper)
Abstract
This is a short survey of the use of intersection types for reasoning in a finitary way about terms interpretations in various models of lambda-calculus.
Cite as
Simona Ronchi Della Rocca. Intersection Types and Denotational Semantics: An Extended Abstract (Invited Paper). In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 2:1-2:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{ronchidellarocca:LIPIcs.TYPES.2016.2,
author = {Ronchi Della Rocca, Simona},
title = {{Intersection Types and Denotational Semantics: An Extended Abstract}},
booktitle = {22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
pages = {2:1--2:7},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-065-1},
ISSN = {1868-8969},
year = {2018},
volume = {97},
editor = {Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.2},
URN = {urn:nbn:de:0030-drops-98614},
doi = {10.4230/LIPIcs.TYPES.2016.2},
annote = {Keywords: Lambda-calculus, Lambda-models, Intersection types}
}
Document
A Normalizing Computation Rule for Propositional Extensionality in Higher-Order Minimal Logic
Abstract
The univalence axiom expresses the principle of extensionality for dependent type theory. However, if we simply add the univalence axiom to type theory, then we lose the property of canonicity - that every closed term computes to a canonical form. A computation becomes "stuck" when it reaches the point that it needs to evaluate a proof term that is an application of the univalence axiom. So we wish to find a way to compute with the univalence axiom. While this problem has been solved with the formulation of cubical type theory, where the computations are expressed using a nominal extension of lambda-calculus, it may be interesting to explore alternative solutions, which do not require such an extension.
As a first step, we present here a system of propositional higher-order minimal logic (PHOML). There are three kinds of typing judgement in PHOML. There are terms which inhabit types, which are the simple types over Omega. There are proofs which inhabit propositions, which are the terms of type Omega. The canonical propositions are those constructed from false by implication. Thirdly, there are paths which inhabit equations M =_A N, where M and N are terms of type A. There are two ways to prove an equality: reflexivity, and propositional extensionality - logically equivalent propositions are equal. This system allows for some definitional equalities that are not present in cubical type theory, namely that transport along the trivial path is identity.
We present a call-by-name reduction relation for this system, and prove that the system satisfies canonicity: every closed typable term head-reduces to a canonical form. This work has been formalised in Agda.
Cite as
Robin Adams, Marc Bezem, and Thierry Coquand. A Normalizing Computation Rule for Propositional Extensionality in Higher-Order Minimal Logic. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 3:1-3:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{adams_et_al:LIPIcs.TYPES.2016.3,
author = {Adams, Robin and Bezem, Marc and Coquand, Thierry},
title = {{A Normalizing Computation Rule for Propositional Extensionality in Higher-Order Minimal Logic}},
booktitle = {22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
pages = {3:1--3:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-065-1},
ISSN = {1868-8969},
year = {2018},
volume = {97},
editor = {Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.3},
URN = {urn:nbn:de:0030-drops-98581},
doi = {10.4230/LIPIcs.TYPES.2016.3},
annote = {Keywords: type theory, univalence, canonicity}
}
Document
On Natural Deduction for Herbrand Constructive Logics II: Curry-Howard Correspondence for Markov's Principle in First-Order Logic and Arithmetic
Abstract
Intuitionistic first-order logic extended with a restricted form of Markov's principle is constructive and admits a Curry-Howard correspondence, as shown by Herbelin. We provide a simpler proof of that result and then we study intuitionistic first-order logic extended with unrestricted Markov's principle. Starting from classical natural deduction, we restrict the excluded middle and we obtain a natural deduction system and a parallel Curry-Howard isomorphism for the logic. We show that proof terms for existentially quantified formulas reduce to a list of individual terms representing all possible witnesses. As corollary, we derive that the logic is Herbrand constructive: whenever it proves any existential formula, it proves also an Herbrand disjunction for the formula. Finally, using the techniques just introduced, we also provide a new computational interpretation of Arithmetic with Markov's principle.
Cite as
Federico Aschieri and Matteo Manighetti. On Natural Deduction for Herbrand Constructive Logics II: Curry-Howard Correspondence for Markov's Principle in First-Order Logic and Arithmetic. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 4:1-4:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{aschieri_et_al:LIPIcs.TYPES.2016.4,
author = {Aschieri, Federico and Manighetti, Matteo},
title = {{On Natural Deduction for Herbrand Constructive Logics II: Curry-Howard Correspondence for Markov's Principle in First-Order Logic and Arithmetic}},
booktitle = {22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
pages = {4:1--4:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-065-1},
ISSN = {1868-8969},
year = {2018},
volume = {97},
editor = {Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.4},
URN = {urn:nbn:de:0030-drops-98590},
doi = {10.4230/LIPIcs.TYPES.2016.4},
annote = {Keywords: Markov's Principle, first-order logic, natural deduction, Curry-Howard}
}
Document
Design and Implementation of the Andromeda Proof Assistant
Abstract
Andromeda is an LCF-style proof assistant where the user builds derivable judgments by writing code in a meta-level programming language AML. The only trusted component of Andromeda is a minimalist nucleus (an implementation of the inference rules of an object-level type theory), which controls construction and decomposition of type-theoretic judgments.
Since the nucleus does not perform complex tasks like equality checking beyond syntactic equality, this responsibility is delegated to the user, who implements one or more equality checking procedures in the meta-language. The AML interpreter requests witnesses of equality from user code using the mechanism of algebraic operations and handlers. Dynamic checks in the nucleus guarantee that no invalid object-level derivations can be constructed.
To demonstrate the flexibility of this system structure, we implemented a nucleus consisting of dependent type theory with equality reflection. Equality reflection provides a very high level of expressiveness, as it allows the user to add new judgmental equalities, but it also destroys desirable meta-theoretic properties of type theory (such as decidability and strong normalization).
The power of effects and handlers in AML is demonstrated by a standard library that provides default algorithms for equality checking, computation of normal forms, and implicit argument filling. Users can extend these new algorithms by providing local "hints" or by completely replacing these algorithms for particular developments. We demonstrate the resulting system by showing how to axiomatize and compute with natural numbers, by axiomatizing the untyped lambda-calculus, and by implementing a simple automated system for managing a universe of types.
Cite as
Andrej Bauer, Gaëtan Gilbert, Philipp G. Haselwarter, Matija Pretnar, and Christopher A. Stone. Design and Implementation of the Andromeda Proof Assistant. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 5:1-5:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{bauer_et_al:LIPIcs.TYPES.2016.5,
author = {Bauer, Andrej and Gilbert, Ga\"{e}tan and Haselwarter, Philipp G. and Pretnar, Matija and Stone, Christopher A.},
title = {{Design and Implementation of the Andromeda Proof Assistant}},
booktitle = {22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
pages = {5:1--5:31},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-065-1},
ISSN = {1868-8969},
year = {2018},
volume = {97},
editor = {Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.5},
URN = {urn:nbn:de:0030-drops-98574},
doi = {10.4230/LIPIcs.TYPES.2016.5},
annote = {Keywords: type theory, proof assistant, equality reflection, computational effects}
}
Document
Realizability at Work: Separating Two Constructive Notions of Finiteness
Abstract
We elaborate in detail a realizability model for Martin-Löf dependent type theory with the purpose to analyze a subtle distinction between two constructive notions of finiteness of a set A. The two notions are: (1) A is Noetherian: the empty list can be constructed from lists over A containing duplicates by a certain inductive shortening process; (2) A is streamless: every enumeration of A contains a duplicate.
Cite as
Marc Bezem, Thierry Coquand, Keiko Nakata, and Erik Parmann. Realizability at Work: Separating Two Constructive Notions of Finiteness. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 6:1-6:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{bezem_et_al:LIPIcs.TYPES.2016.6,
author = {Bezem, Marc and Coquand, Thierry and Nakata, Keiko and Parmann, Erik},
title = {{Realizability at Work: Separating Two Constructive Notions of Finiteness}},
booktitle = {22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
pages = {6:1--6:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-065-1},
ISSN = {1868-8969},
year = {2018},
volume = {97},
editor = {Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.6},
URN = {urn:nbn:de:0030-drops-98541},
doi = {10.4230/LIPIcs.TYPES.2016.6},
annote = {Keywords: Type theory, realizability, constructive notions of finiteness}
}
Document
Parametricity, Automorphisms of the Universe, and Excluded Middle
Abstract
It is known that one can construct non-parametric functions by assuming classical axioms. Our work is a converse to that: we prove classical axioms in dependent type theory assuming specific instances of non-parametricity. We also address the interaction between classical axioms and the existence of automorphisms of a type universe. We work over intensional Martin-Löf dependent type theory, and for some results assume further principles including function extensionality, propositional extensionality, propositional truncation, and the univalence axiom.
Cite as
Auke B. Booij, Martín H. Escardó, Peter LeFanu Lumsdaine, and Michael Shulman. Parametricity, Automorphisms of the Universe, and Excluded Middle. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 7:1-7:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{booij_et_al:LIPIcs.TYPES.2016.7,
author = {Booij, Auke B. and Escard\'{o}, Mart{\'\i}n H. and Lumsdaine, Peter LeFanu and Shulman, Michael},
title = {{Parametricity, Automorphisms of the Universe, and Excluded Middle}},
booktitle = {22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
pages = {7:1--7:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-065-1},
ISSN = {1868-8969},
year = {2018},
volume = {97},
editor = {Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.7},
URN = {urn:nbn:de:0030-drops-98554},
doi = {10.4230/LIPIcs.TYPES.2016.7},
annote = {Keywords: relational parametricity, dependent type theory, univalent foundations, homotopy type theory, excluded middle, classical mathematics, constructive mat}
}
Document
Coq Support in HAHA
Abstract
HAHA is a tool that helps in teaching and learning Hoare logic. It is targeted at an introductory course on software verification. We present a set of new features of the HAHA verification environment that exploit Coq. These features are (1) generation of verification conditions in Coq so that they can be explored and proved interactively and (2) compilation of HAHA programs into CompCert certified compilation tool-chain.
With the interactive Coq proving support we obtain an interesting functionality that makes it possible to carefully examine step-by-step verification conditions and systematically discover flaws in their formulation. As a result Coq back-end serves as a kind of specification debugger.
Cite as
Jacek Chrzaszcz, Aleksy Schubert, and Jakub Zakrzewski. Coq Support in HAHA. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 8:1-8:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{chrzaszcz_et_al:LIPIcs.TYPES.2016.8,
author = {Chrzaszcz, Jacek and Schubert, Aleksy and Zakrzewski, Jakub},
title = {{Coq Support in HAHA}},
booktitle = {22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
pages = {8:1--8:26},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-065-1},
ISSN = {1868-8969},
year = {2018},
volume = {97},
editor = {Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.8},
URN = {urn:nbn:de:0030-drops-98562},
doi = {10.4230/LIPIcs.TYPES.2016.8},
annote = {Keywords: Hoare logic, program verification, Coq theorem prover, teaching}
}
Document
A Shallow Embedding of Pure Type Systems into First-Order Logic
Abstract
We define a shallow embedding of logical proof-irrelevant Pure Type Systems (piPTSs) into minimal first-order logic. In logical piPTSs a distinguished sort *^p of propositions is assumed. Given a context Gamma and a Gamma-proposition tau, i.e., a term tau such that Gamma |- tau : *^p, the embedding translates tau and Gamma into a first-order formula F_Gamma(tau) and a set of first-order axioms Delta_Gamma. The embedding is not complete in general, but it is strong enough to correctly translate most of piPTS propositions (by completeness we mean that if Gamma |- M : tau is derivable in the piPTS then F_Gamma(tau) is provable in minimal first-order logic from the axioms Delta_Gamma). We show the embedding to be sound, i.e., if F_Gamma(tau) is provable in minimal first-order logic from the axioms Delta_Gamma, then Gamma |- M : tau is derivable in the original system for some term M. The interest in the proposed embedding stems from the fact that it forms a basis of the translations used in the recently developed CoqHammer automation tool for dependent type theory.
Cite as
Lukasz Czajka. A Shallow Embedding of Pure Type Systems into First-Order Logic. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 9:1-9:39, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{czajka:LIPIcs.TYPES.2016.9,
author = {Czajka, Lukasz},
title = {{A Shallow Embedding of Pure Type Systems into First-Order Logic}},
booktitle = {22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
pages = {9:1--9:39},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-065-1},
ISSN = {1868-8969},
year = {2018},
volume = {97},
editor = {Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.9},
URN = {urn:nbn:de:0030-drops-98533},
doi = {10.4230/LIPIcs.TYPES.2016.9},
annote = {Keywords: pure type systems, first-order logic, hammers, proof automation, dependent type theory}
}
Document
Permutability in Proof Terms for Intuitionistic Sequent Calculus with Cuts
Abstract
This paper gives a comprehensive and coherent view on permutability in the intuitionistic sequent calculus with cuts. Specifically we show that, once permutability is packaged into appropriate global reduction procedures, it organizes the internal structure of the system and determines fragments with computational interest, both for the computation-as-proof-normalization and the computation-as-proof-search paradigms. The vehicle of the study is a lambda-calculus of multiary proof terms with generalized application, previously developed by the authors (the paper argues this system represents the simplest fragment of ordinary sequent calculus that does not fall into mere natural deduction). We start by adapting to our setting the concept of normal proof, developed by Mints, Dyckhoff, and Pinto, and by defining natural proofs, so that a proof is normal iff it is natural and cut-free. Natural proofs form a subsystem with a transparent Curry-Howard interpretation (a kind of formal vector notation for lambda-terms with vectors consisting of lists of lists of arguments), while searching for normal proofs corresponds to a slight relaxation of focusing (in the sense of LJT). Next, we define a process of permutative conversion to natural form, and show that its combination with cut elimination gives a concept of normalization for the sequent calculus. We derive a systematic picture of the full system comprehending a rich set of reduction procedures (cut elimination, flattening, permutative conversion, normalization, focalization), organizing the relevant subsystems and the important subclasses of cut-free, normal, and focused proofs.
Cite as
José Espírito Santo, Maria João Frade, and Luís Pinto. Permutability in Proof Terms for Intuitionistic Sequent Calculus with Cuts. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 10:1-10:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{espiritosanto_et_al:LIPIcs.TYPES.2016.10,
author = {Esp{\'\i}rito Santo, Jos\'{e} and Frade, Maria Jo\~{a}o and Pinto, Lu{\'\i}s},
title = {{Permutability in Proof Terms for Intuitionistic Sequent Calculus with Cuts}},
booktitle = {22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
pages = {10:1--10:27},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-065-1},
ISSN = {1868-8969},
year = {2018},
volume = {97},
editor = {Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.10},
URN = {urn:nbn:de:0030-drops-98523},
doi = {10.4230/LIPIcs.TYPES.2016.10},
annote = {Keywords: sequent calculus, permutative conversion, Curry-Howard isomorphism, vector of arguments, generalized application, normal proof, natural proof, cut eli}
}
Document
Covering Spaces in Homotopy Type Theory
Abstract
Broadly speaking, algebraic topology consists of associating algebraic structures to topological spaces that give information about their structure. An elementary, but fundamental, example is provided by the theory of covering spaces, which associate groups to covering spaces in such a way that the universal cover corresponds to the fundamental group of the space. One natural question to ask is whether these connections can be stated in homotopy type theory, a new area linking type theory to homotopy theory. In this paper, we give an affirmative answer with a surprisingly concise definition of covering spaces in type theory; we are able to prove various expected properties about the newly defined covering spaces, including the connections with fundamental groups. An additional merit is that our work has been fully mechanized in the proof assistant Agda.
Cite as
Kuen-Bang Hou (Favonia) and Robert Harper. Covering Spaces in Homotopy Type Theory. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 11:1-11:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{hou(favonia)_et_al:LIPIcs.TYPES.2016.11,
author = {Hou (Favonia), Kuen-Bang and Harper, Robert},
title = {{Covering Spaces in Homotopy Type Theory}},
booktitle = {22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
pages = {11:1--11:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-065-1},
ISSN = {1868-8969},
year = {2018},
volume = {97},
editor = {Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.11},
URN = {urn:nbn:de:0030-drops-98512},
doi = {10.4230/LIPIcs.TYPES.2016.11},
annote = {Keywords: homotopy type theory, covering space, fundamental group, mechanized reasoning}
}
Document
Defining Trace Semantics for CSP-Agda
Abstract
This article is based on the library CSP-Agda, which represents the process algebra CSP coinductively in the interactive theorem prover Agda. The intended application area of CSP-Agda is the proof of properties of safety critical systems (especially the railway domain). In CSP-Agda, CSP processes have been extended to monadic form, allowing the design of processes in a more modular way. In this article we extend the trace semantics of CSP to the monadic setting. We implement this semantics, together with the corresponding refinement and equality relation, formally in CSP-Agda. In order to demonstrate the proof capabilities of CSP-Agda, we prove in CSP-Agda selected algebraic laws of CSP based on the trace semantics. Because of the monadic settings, some adjustments need to be made to these laws. The examples covered in this article are the laws of refinement, commutativity of interleaving and parallel, and the monad laws for the monadic extension of CSP. All proofs and definitions have been type checked in Agda. Further proofs of algebraic laws will be available in the repository of CSP-Agda.
Cite as
Bashar Igried and Anton Setzer. Defining Trace Semantics for CSP-Agda. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 12:1-12:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{igried_et_al:LIPIcs.TYPES.2016.12,
author = {Igried, Bashar and Setzer, Anton},
title = {{Defining Trace Semantics for CSP-Agda}},
booktitle = {22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
pages = {12:1--12:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-065-1},
ISSN = {1868-8969},
year = {2018},
volume = {97},
editor = {Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.12},
URN = {urn:nbn:de:0030-drops-98509},
doi = {10.4230/LIPIcs.TYPES.2016.12},
annote = {Keywords: Agda, CSP, Coalgebras, Coinductive Data Types, Dependent Type Theory, IO-Monad, Induction-Recursion, Interactive Program, Monad, Monadic Programming,}
}
Document
On Subtyping in Type Theories with Canonical Objects
Abstract
How should one introduce subtyping into type theories with canonical objects such as Martin-Löf's type theory? It is known that the usual subsumptive subtyping is inadequate and it is understood, at least theoretically, that coercive subtyping should instead be employed. However, it has not been studied what the proper coercive subtyping mechanism is and how it should be used to capture intuitive notions of subtyping. In this paper, we introduce a type system with signatures where coercive subtyping relations can be specified, and argue that this provides a suitable subtyping mechanism for type theories with canonical objects. In particular, we show that the subtyping extension is well-behaved by relating it to the previous formulation of coercive subtyping. The paper then proceeds to study the connection with intuitive notions of subtyping. It first shows how a subsumptive subtyping system can be embedded faithfully. Then, it studies how Russell-style universe inclusions can be understood as coercions in our system. And finally, we study constructor subtyping as an example to illustrate that, sometimes, injectivity of coercions need be assumed in order to capture properly some notions of subtyping.
Cite as
Georgiana Elena Lungu and Zhaohui Luo. On Subtyping in Type Theories with Canonical Objects. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 13:1-13:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{lungu_et_al:LIPIcs.TYPES.2016.13,
author = {Lungu, Georgiana Elena and Luo, Zhaohui},
title = {{On Subtyping in Type Theories with Canonical Objects}},
booktitle = {22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
pages = {13:1--13:31},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-065-1},
ISSN = {1868-8969},
year = {2018},
volume = {97},
editor = {Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.13},
URN = {urn:nbn:de:0030-drops-98496},
doi = {10.4230/LIPIcs.TYPES.2016.13},
annote = {Keywords: subtyping, type theory, conservative extension, canonical objects}
}
Document
A Formal Study of Boolean Games with Random Formulas as Payoff Functions
Abstract
In this paper, we present a probabilistic analysis of Boolean games. We consider the class of Boolean games where payoff functions are given by random Boolean formulas. This permits to study certain properties of this class in its totality, such as the probability of existence of a winning strategy, including its asymptotic behaviour. With the help of the Coq proof assistant, we develop a Coq library of Boolean games, to provide a formal proof of our results, and a basis for further developments.
Cite as
Érik Martin-Dorel and Sergei Soloviev. A Formal Study of Boolean Games with Random Formulas as Payoff Functions. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 14:1-14:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{martindorel_et_al:LIPIcs.TYPES.2016.14,
author = {Martin-Dorel, \'{E}rik and Soloviev, Sergei},
title = {{A Formal Study of Boolean Games with Random Formulas as Payoff Functions}},
booktitle = {22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
pages = {14:1--14:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-065-1},
ISSN = {1868-8969},
year = {2018},
volume = {97},
editor = {Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.14},
URN = {urn:nbn:de:0030-drops-98486},
doi = {10.4230/LIPIcs.TYPES.2016.14},
annote = {Keywords: Boolean games, Random process, Coq formal proofs}
}
Document
The Completeness of BCD for an Operational Semantics
Abstract
We give a completeness theorem for the BCD theory of intersection types in an operational semantics based on logical relations.
Cite as
Richard Statman. The Completeness of BCD for an Operational Semantics. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 15:1-15:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{statman:LIPIcs.TYPES.2016.15,
author = {Statman, Richard},
title = {{The Completeness of BCD for an Operational Semantics}},
booktitle = {22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
pages = {15:1--15:5},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-065-1},
ISSN = {1868-8969},
year = {2018},
volume = {97},
editor = {Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.15},
URN = {urn:nbn:de:0030-drops-98478},
doi = {10.4230/LIPIcs.TYPES.2016.15},
annote = {Keywords: intersection types, operational semantics, Beth model, logical relations, forcing}
}