Volume
LIPIcs, Volume 104
23rd International Conference on Types for Proofs and Programs (TYPES 2017)
Event
TYPES 2017, May 29 to June 1, 2017, Budapest, HungaryEditors
Publication Details
- published at: 2019-01-08
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-071-2
- DBLP: db/conf/types/types2017
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 104, TYPES'17, Complete Volume
Abstract
LIPIcs, Volume 104, TYPES'17, Complete Volume
Cite as
23rd International Conference on Types for Proofs and Programs (TYPES 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 104, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@Proceedings{abel_et_al:LIPIcs.TYPES.2017,
title = {{LIPIcs, Volume 104, TYPES'17, Complete Volume}},
booktitle = {23rd International Conference on Types for Proofs and Programs (TYPES 2017)},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-071-2},
ISSN = {1868-8969},
year = {2019},
volume = {104},
editor = {Abel, Andreas and Nordvall Forsberg, Fredrik and Kaposi, Ambrus},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2017},
URN = {urn:nbn:de:0030-drops-101671},
doi = {10.4230/LIPIcs.TYPES.2017},
annote = {Keywords: Theory of computation, Type theory, Proof theory, Program verification}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
23rd International Conference on Types for Proofs and Programs (TYPES 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 104, pp. 0:i-0:x, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{abel_et_al:LIPIcs.TYPES.2017.0,
author = {Abel, Andreas and Nordvall Forsberg, Fredrik and Kaposi, Ambrus},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {23rd International Conference on Types for Proofs and Programs (TYPES 2017)},
pages = {0:i--0:x},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-071-2},
ISSN = {1868-8969},
year = {2019},
volume = {104},
editor = {Abel, Andreas and Nordvall Forsberg, Fredrik and Kaposi, Ambrus},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2017.0},
URN = {urn:nbn:de:0030-drops-100488},
doi = {10.4230/LIPIcs.TYPES.2017.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic
Abstract
We start from an untyped, well-scoped lambda-calculus and introduce a bidirectional typing relation corresponding to a Multiplicative-Additive Intuitionistic Linear Logic. We depart from typical presentations to adopt one that is well-suited to the intensional setting of Martin-Löf Type Theory. This relation is based on the idea that a linear term consumes some of the resources available in its context whilst leaving behind leftovers which can then be fed to another program.
Concretely, this means that typing derivations have both an input and an output context. This leads to a notion of weakening (the extra resources added to the input context come out unchanged in the output one), a rather direct proof of stability under substitution, an analogue of the frame rule of separation logic showing that the state of unused resources can be safely ignored, and a proof that typechecking is decidable. Finally, we demonstrate that this alternative formalization is sound and complete with respect to a more traditional representation of Intuitionistic Linear Logic.
The work has been fully formalised in Agda, commented source files are provided as additional material available at https://github.com/gallais/typing-with-leftovers.
Cite as
Guillaume Allais. Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic. In 23rd International Conference on Types for Proofs and Programs (TYPES 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 104, pp. 1:1-1:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{allais:LIPIcs.TYPES.2017.1,
author = {Allais, Guillaume},
title = {{Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic}},
booktitle = {23rd International Conference on Types for Proofs and Programs (TYPES 2017)},
pages = {1:1--1:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-071-2},
ISSN = {1868-8969},
year = {2019},
volume = {104},
editor = {Abel, Andreas and Nordvall Forsberg, Fredrik and Kaposi, Ambrus},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2017.1},
URN = {urn:nbn:de:0030-drops-100490},
doi = {10.4230/LIPIcs.TYPES.2017.1},
annote = {Keywords: Type System, Bidirectional, Linear Logic, Agda}
}
Document
Lower End of the Linial-Post Spectrum
Abstract
We show that recognizing axiomatizations of the Hilbert-style calculus containing only the axiom a -> (b -> a) is undecidable (a reduction from the Post correspondence problem is formalized in the Lean theorem prover). Interestingly, the problem remains undecidable considering only axioms which, when seen as simple types, are principal for some lambda-terms in beta-normal form. This problem is closely related to type-based composition synthesis, i.e. finding a composition of given building blocks (typed terms) satisfying a desired specification (goal type).
Contrary to the above result, axiomatizations of the Hilbert-style calculus containing only the axiom a -> (b -> b) are recognizable in linear time.
Cite as
Andrej Dudenhefner and Jakob Rehof. Lower End of the Linial-Post Spectrum. In 23rd International Conference on Types for Proofs and Programs (TYPES 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 104, pp. 2:1-2:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{dudenhefner_et_al:LIPIcs.TYPES.2017.2,
author = {Dudenhefner, Andrej and Rehof, Jakob},
title = {{Lower End of the Linial-Post Spectrum}},
booktitle = {23rd International Conference on Types for Proofs and Programs (TYPES 2017)},
pages = {2:1--2:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-071-2},
ISSN = {1868-8969},
year = {2019},
volume = {104},
editor = {Abel, Andreas and Nordvall Forsberg, Fredrik and Kaposi, Ambrus},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2017.2},
URN = {urn:nbn:de:0030-drops-100503},
doi = {10.4230/LIPIcs.TYPES.2017.2},
annote = {Keywords: combinatory logic, lambda calculus, type theory, simple types, inhabitation, principal type}
}
Document
Proof Terms for Generalized Natural Deduction
Abstract
In previous work it has been shown how to generate natural deduction rules for propositional connectives from truth tables, both for classical and constructive logic. The present paper extends this for the constructive case with proof-terms, thereby extending the Curry-Howard isomorphism to these new connectives. A general notion of conversion of proofs is defined, both as a conversion of derivations and as a reduction of proof-terms. It is shown how the well-known rules for natural deduction (Gentzen, Prawitz) and general elimination rules (Schroeder-Heister, von Plato, and others), and their proof conversions can be found as instances. As an illustration of the power of the method, we give constructive rules for the nand logical operator (also called Sheffer stroke).
As usual, conversions come in two flavours: either a detour conversion arising from a detour convertibility, where an introduction rule is immediately followed by an elimination rule, or a permutation conversion arising from an permutation convertibility, an elimination rule nested inside another elimination rule. In this paper, both are defined for the general setting, as conversions of derivations and as reductions of proof-terms. The properties of these are studied as proof-term reductions. As one of the main contributions it is proved that detour conversion is strongly normalizing and permutation conversion is strongly normalizing: no matter how one reduces, the process eventually terminates. Furthermore, the combination of the two conversions is shown to be weakly normalizing: one can always reduce away all convertibilities.
Cite as
Herman Geuvers and Tonny Hurkens. Proof Terms for Generalized Natural Deduction. In 23rd International Conference on Types for Proofs and Programs (TYPES 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 104, pp. 3:1-3:39, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{geuvers_et_al:LIPIcs.TYPES.2017.3,
author = {Geuvers, Herman and Hurkens, Tonny},
title = {{Proof Terms for Generalized Natural Deduction}},
booktitle = {23rd International Conference on Types for Proofs and Programs (TYPES 2017)},
pages = {3:1--3:39},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-071-2},
ISSN = {1868-8969},
year = {2019},
volume = {104},
editor = {Abel, Andreas and Nordvall Forsberg, Fredrik and Kaposi, Ambrus},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2017.3},
URN = {urn:nbn:de:0030-drops-100519},
doi = {10.4230/LIPIcs.TYPES.2017.3},
annote = {Keywords: constructive logic, natural deduction, detour conversion, permutation conversion, normalization Curry-Howard isomorphism}
}
Document
PML2: Integrated Program Verification in ML
Abstract
We present the PML_2 language, which provides a uniform environment for programming, and for proving properties of programs in an ML-like setting. The language is Curry-style and call-by-value, it provides a control operator (interpreted in terms of classical logic), it supports general recursion and a very general form of (implicit, non-coercive) subtyping. In the system, equational properties of programs are expressed using two new type formers, and they are proved by constructing terminating programs. Although proofs rely heavily on equational reasoning, equalities are exclusively managed by the type-checker. This means that the user only has to choose which equality to use, and not where to use it, as is usually done in mathematical proofs. In the system, writing proofs mostly amounts to applying lemmas (possibly recursive function calls), and to perform case analyses (pattern matchings).
Cite as
Rodolphe Lepigre. PML2: Integrated Program Verification in ML. In 23rd International Conference on Types for Proofs and Programs (TYPES 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 104, pp. 4:1-4:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{lepigre:LIPIcs.TYPES.2017.4,
author = {Lepigre, Rodolphe},
title = {{PML2: Integrated Program Verification in ML}},
booktitle = {23rd International Conference on Types for Proofs and Programs (TYPES 2017)},
pages = {4:1--4:27},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-071-2},
ISSN = {1868-8969},
year = {2019},
volume = {104},
editor = {Abel, Andreas and Nordvall Forsberg, Fredrik and Kaposi, Ambrus},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2017.4},
URN = {urn:nbn:de:0030-drops-100521},
doi = {10.4230/LIPIcs.TYPES.2017.4},
annote = {Keywords: program verification, classical logic, ML-like language, termination checking, Curry-style quantification, implicit subtyping}
}
Document
Formalized Proof Systems for Propositional Logic
Abstract
We have formalized a range of proof systems for classical propositional logic (sequent calculus, natural deduction, Hilbert systems, resolution) in Isabelle/HOL and have proved the most important meta-theoretic results about semantics and proofs: compactness, soundness, completeness, translations between proof systems, cut-elimination, interpolation and model existence.
Cite as
Julius Michaelis and Tobias Nipkow. Formalized Proof Systems for Propositional Logic. In 23rd International Conference on Types for Proofs and Programs (TYPES 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 104, pp. 5:1-5:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{michaelis_et_al:LIPIcs.TYPES.2017.5,
author = {Michaelis, Julius and Nipkow, Tobias},
title = {{Formalized Proof Systems for Propositional Logic}},
booktitle = {23rd International Conference on Types for Proofs and Programs (TYPES 2017)},
pages = {5:1--5:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-071-2},
ISSN = {1868-8969},
year = {2019},
volume = {104},
editor = {Abel, Andreas and Nordvall Forsberg, Fredrik and Kaposi, Ambrus},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2017.5},
URN = {urn:nbn:de:0030-drops-100537},
doi = {10.4230/LIPIcs.TYPES.2017.5},
annote = {Keywords: formalization of logic, proof systems, sequent calculus, natural deduction, resolution}
}
Document
Decomposing the Univalence Axiom
Abstract
This paper investigates Voevodsky's univalence axiom in intensional Martin-Löf type theory. In particular, it looks at how univalence can be derived from simpler axioms. We first present some existing work, collected together from various published and unpublished sources; we then present a new decomposition of the univalence axiom into simpler axioms. We argue that these axioms are easier to verify in certain potential models of univalent type theory, particularly those models based on cubical sets. Finally we show how this decomposition is relevant to an open problem in type theory.
Cite as
Ian Orton and Andrew M. Pitts. Decomposing the Univalence Axiom. In 23rd International Conference on Types for Proofs and Programs (TYPES 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 104, pp. 6:1-6:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{orton_et_al:LIPIcs.TYPES.2017.6,
author = {Orton, Ian and Pitts, Andrew M.},
title = {{Decomposing the Univalence Axiom}},
booktitle = {23rd International Conference on Types for Proofs and Programs (TYPES 2017)},
pages = {6:1--6:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-071-2},
ISSN = {1868-8969},
year = {2019},
volume = {104},
editor = {Abel, Andreas and Nordvall Forsberg, Fredrik and Kaposi, Ambrus},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2017.6},
URN = {urn:nbn:de:0030-drops-100546},
doi = {10.4230/LIPIcs.TYPES.2017.6},
annote = {Keywords: dependent type theory, homotopy type theory, univalent type theory, univalence, cubical type theory, cubical sets}
}
Document
On Equality of Objects in Categories in Constructive Type Theory
Abstract
In this note we remark on the problem of equality of objects in categories formalized in Martin-Löf's constructive type theory. A standard notion of category in this system is E-category, where no such equality is specified. The main observation here is that there is no general extension of E-categories to categories with equality on objects, unless the principle Uniqueness of Identity Proofs (UIP) holds. We also introduce the notion of an H-category with equality on objects, which makes it easy to compare to the notion of univalent category proposed for Univalent Type Theory by Ahrens, Kapulkin and Shulman.
Cite as
Erik Palmgren. On Equality of Objects in Categories in Constructive Type Theory. In 23rd International Conference on Types for Proofs and Programs (TYPES 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 104, pp. 7:1-7:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{palmgren:LIPIcs.TYPES.2017.7,
author = {Palmgren, Erik},
title = {{On Equality of Objects in Categories in Constructive Type Theory}},
booktitle = {23rd International Conference on Types for Proofs and Programs (TYPES 2017)},
pages = {7:1--7:7},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-071-2},
ISSN = {1868-8969},
year = {2019},
volume = {104},
editor = {Abel, Andreas and Nordvall Forsberg, Fredrik and Kaposi, Ambrus},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2017.7},
URN = {urn:nbn:de:0030-drops-100553},
doi = {10.4230/LIPIcs.TYPES.2017.7},
annote = {Keywords: type theory, formalization, category theory, setoids}
}