eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-01-08
104
0
0
10.4230/LIPIcs.TYPES.2017
article
LIPIcs, Volume 104, TYPES'17, Complete Volume
Abel, Andreas
Nordvall Forsberg, Fredrik
Kaposi, Ambrus
LIPIcs, Volume 104, TYPES'17, Complete Volume
https://drops.dagstuhl.de/storage/00lipics/lipics-vol104-types2017/LIPIcs.TYPES.2017/LIPIcs.TYPES.2017.pdf
Theory of computation, Type theory, Proof theory, Program verification
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-01-08
104
0:i
0:x
10.4230/LIPIcs.TYPES.2017.0
article
Front Matter, Table of Contents, Preface, Conference Organization
Abel, Andreas
Nordvall Forsberg, Fredrik
Kaposi, Ambrus
Front Matter, Table of Contents, Preface, Conference Organization
https://drops.dagstuhl.de/storage/00lipics/lipics-vol104-types2017/LIPIcs.TYPES.2017.0/LIPIcs.TYPES.2017.0.pdf
Front Matter
Table of Contents
Preface
Conference Organization
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-01-08
104
1:1
1:22
10.4230/LIPIcs.TYPES.2017.1
article
Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic
Allais, Guillaume
1
iCIS, Radboud University Nijmegen, The Netherlands
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol104-types2017/LIPIcs.TYPES.2017.1/LIPIcs.TYPES.2017.1.pdf
Type System
Bidirectional
Linear Logic
Agda
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-01-08
104
2:1
2:15
10.4230/LIPIcs.TYPES.2017.2
article
Lower End of the Linial-Post Spectrum
Dudenhefner, Andrej
1
Rehof, Jakob
1
Technical University of Dortmund, Dortmund, Germany
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol104-types2017/LIPIcs.TYPES.2017.2/LIPIcs.TYPES.2017.2.pdf
combinatory logic
lambda calculus
type theory
simple types
inhabitation
principal type
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-01-08
104
3:1
3:39
10.4230/LIPIcs.TYPES.2017.3
article
Proof Terms for Generalized Natural Deduction
Geuvers, Herman
1
Hurkens, Tonny
1
Radboud University Nijmegen & Technical University Eindhoven, The Netherlands
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol104-types2017/LIPIcs.TYPES.2017.3/LIPIcs.TYPES.2017.3.pdf
constructive logic
natural deduction
detour conversion
permutation conversion
normalization Curry-Howard isomorphism
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-01-08
104
4:1
4:27
10.4230/LIPIcs.TYPES.2017.4
article
PML2: Integrated Program Verification in ML
Lepigre, Rodolphe
1
https://orcid.org/0000-0002-2849-5338
LAMA, CNRS, Université Savoie Mont Blanc, France & , Inria, LSV, CNRS, Université Paris-Saclay, France
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).
https://drops.dagstuhl.de/storage/00lipics/lipics-vol104-types2017/LIPIcs.TYPES.2017.4/LIPIcs.TYPES.2017.4.pdf
program verification
classical logic
ML-like language
termination checking
Curry-style quantification
implicit subtyping
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-01-08
104
5:1
5:16
10.4230/LIPIcs.TYPES.2017.5
article
Formalized Proof Systems for Propositional Logic
Michaelis, Julius
1
https://orcid.org/0000-0003-4626-3722
Nipkow, Tobias
1
https://orcid.org/0000-0003-0730-515X
Technische Universität München, Germany
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol104-types2017/LIPIcs.TYPES.2017.5/LIPIcs.TYPES.2017.5.pdf
formalization of logic
proof systems
sequent calculus
natural deduction
resolution
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-01-08
104
6:1
6:19
10.4230/LIPIcs.TYPES.2017.6
article
Decomposing the Univalence Axiom
Orton, Ian
1
https://orcid.org/0000-0002-9924-0623
Pitts, Andrew M.
1
https://orcid.org/0000-0001-7775-3471
University of Cambridge Dept. Computer Science & Technology, Cambridge, UK
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol104-types2017/LIPIcs.TYPES.2017.6/LIPIcs.TYPES.2017.6.pdf
dependent type theory
homotopy type theory
univalent type theory
univalence
cubical type theory
cubical sets
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-01-08
104
7:1
7:7
10.4230/LIPIcs.TYPES.2017.7
article
On Equality of Objects in Categories in Constructive Type Theory
Palmgren, Erik
1
Department of Mathematics, Stockholm University, Stockholm, Sweden
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol104-types2017/LIPIcs.TYPES.2017.7/LIPIcs.TYPES.2017.7.pdf
type theory
formalization
category theory
setoids