Volume
LIPIcs, Volume 130
24th International Conference on Types for Proofs and Programs (TYPES 2018)
Event
TYPES 2018, June 18-21, 2018, Braga, PortugalEditors
Publication Details
- published at: 2019-11-18
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-106-1
- DBLP: db/conf/types/types2018
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 130, TYPES'18, Complete Volume
Abstract
LIPIcs, Volume 130, TYPES'18, Complete Volume
Cite as
24th International Conference on Types for Proofs and Programs (TYPES 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 130, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@Proceedings{dybjer_et_al:LIPIcs.TYPES.2018,
title = {{LIPIcs, Volume 130, TYPES'18, Complete Volume}},
booktitle = {24th International Conference on Types for Proofs and Programs (TYPES 2018)},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-106-1},
ISSN = {1868-8969},
year = {2019},
volume = {130},
editor = {Dybjer, Peter and Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2018},
URN = {urn:nbn:de:0030-drops-114507},
doi = {10.4230/LIPIcs.TYPES.2018},
annote = {Keywords: Theory of computation,Type theory; Constructive mathematics; Logic and verification; Program verification, Software and its engineering}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
24th International Conference on Types for Proofs and Programs (TYPES 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 130, pp. 0:i-0:x, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{dybjer_et_al:LIPIcs.TYPES.2018.0,
author = {Dybjer, Peter and Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {24th International Conference on Types for Proofs and Programs (TYPES 2018)},
pages = {0:i--0:x},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-106-1},
ISSN = {1868-8969},
year = {2019},
volume = {130},
editor = {Dybjer, Peter and Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2018.0},
URN = {urn:nbn:de:0030-drops-114045},
doi = {10.4230/LIPIcs.TYPES.2018.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Martin Hofmann’s Case for Non-Strictly Positive Data Types
Abstract
We describe the breadth-first traversal algorithm by Martin Hofmann that uses a non-strictly positive data type and carry out a simple verification in an extensional setting. Termination is shown by implementing the algorithm in the strongly normalising extension of system F by Mendler-style recursion. We then analyze the same algorithm by alternative verifications first in an intensional setting using a non-strictly positive inductive definition (not just a non-strictly positive data type), and subsequently by two different algebraic reductions. The verification approaches are compared in terms of notions of simulation and should elucidate the somewhat mysterious algorithm and thus make a case for other uses of non-strictly positive data types. Except for the termination proof, which cannot be formalised in Coq, all proofs were formalised in Coq and some of the algorithms were implemented in Agda and Haskell.
Cite as
Ulrich Berger, Ralph Matthes, and Anton Setzer. Martin Hofmann’s Case for Non-Strictly Positive Data Types. In 24th International Conference on Types for Proofs and Programs (TYPES 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 130, pp. 1:1-1:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{berger_et_al:LIPIcs.TYPES.2018.1,
author = {Berger, Ulrich and Matthes, Ralph and Setzer, Anton},
title = {{Martin Hofmann’s Case for Non-Strictly Positive Data Types}},
booktitle = {24th International Conference on Types for Proofs and Programs (TYPES 2018)},
pages = {1:1--1:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-106-1},
ISSN = {1868-8969},
year = {2019},
volume = {130},
editor = {Dybjer, Peter and Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2018.1},
URN = {urn:nbn:de:0030-drops-114052},
doi = {10.4230/LIPIcs.TYPES.2018.1},
annote = {Keywords: non strictly-positive data types, breadth-first traversal, program verification, Mendler-style recursion, System F, theorem proving, Coq, Agda, Haskell}
}
Document
A Simpler Undecidability Proof for System F Inhabitation
Abstract
Provability in the intuitionistic second-order propositional logic (resp. inhabitation in the polymorphic lambda-calculus) was shown by Löb to be undecidable in 1976. Since the original proof is heavily condensed, Arts in collaboration with Dekkers provided a fully unfolded argument in 1992 spanning approximately fifty pages. Later in 1997, Urzyczyn developed a different, syntax oriented proof. Each of the above approaches embeds (an undecidable fragment of) first-order predicate logic into second-order propositional logic.
In this work, we develop a simpler undecidability proof by reduction from solvability of Diophantine equations (is there an integer solution to P(x_1, ..., x_n) = 0 where P is a polynomial with integer coefficients?). Compared to the previous approaches, the given reduction is more accessible for formalization and more comprehensible for didactic purposes. Additionally, we formalize soundness and completeness of the reduction in the Coq proof assistant under the banner of "type theory inside type theory".
Cite as
Andrej Dudenhefner and Jakob Rehof. A Simpler Undecidability Proof for System F Inhabitation. In 24th International Conference on Types for Proofs and Programs (TYPES 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 130, pp. 2:1-2:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{dudenhefner_et_al:LIPIcs.TYPES.2018.2,
author = {Dudenhefner, Andrej and Rehof, Jakob},
title = {{A Simpler Undecidability Proof for System F Inhabitation}},
booktitle = {24th International Conference on Types for Proofs and Programs (TYPES 2018)},
pages = {2:1--2:11},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-106-1},
ISSN = {1868-8969},
year = {2019},
volume = {130},
editor = {Dybjer, Peter and Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2018.2},
URN = {urn:nbn:de:0030-drops-114061},
doi = {10.4230/LIPIcs.TYPES.2018.2},
annote = {Keywords: System F, Lambda Calculus, Inhabitation, Propositional Logic, Provability, Undecidability, Coq, Formalization}
}
Document
Dependent Sums and Dependent Products in Bishop’s Set Theory
Abstract
According to the standard, non type-theoretic accounts of Bishop’s constructivism (BISH), dependent functions are not necessary to BISH. Dependent functions though, are explicitly used by Bishop in his definition of the intersection of a family of subsets, and they are necessary to the definition of arbitrary products. In this paper we present the basic notions and principles of CSFT, a semi-formal constructive theory of sets and functions intended to be a minimal, adequate and faithful, in Feferman’s sense, semi-formalisation of Bishop’s set theory (BST). We define the notions of dependent sum (or exterior union) and dependent product of set-indexed families of sets within CSFT, and we prove the distributivity of prod over sum i.e., the translation of the type-theoretic axiom of choice within CSFT. We also define the notions of dependent sum (or interior union) and dependent product of set-indexed families of subsets within CSFT. For these definitions we extend BST with the universe of sets #1 V_0 and the universe of functions #1 V_1.
Cite as
Iosif Petrakis. Dependent Sums and Dependent Products in Bishop’s Set Theory. In 24th International Conference on Types for Proofs and Programs (TYPES 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 130, pp. 3:1-3:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{petrakis:LIPIcs.TYPES.2018.3,
author = {Petrakis, Iosif},
title = {{Dependent Sums and Dependent Products in Bishop’s Set Theory}},
booktitle = {24th International Conference on Types for Proofs and Programs (TYPES 2018)},
pages = {3:1--3:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-106-1},
ISSN = {1868-8969},
year = {2019},
volume = {130},
editor = {Dybjer, Peter and Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2018.3},
URN = {urn:nbn:de:0030-drops-114070},
doi = {10.4230/LIPIcs.TYPES.2018.3},
annote = {Keywords: Bishop’s constructive mathematics, Martin-L\"{o}f’s type theory, dependent sums, dependent products, type-theoretic axiom of choice}
}
Document
Semantic Subtyping for Non-Strict Languages
Abstract
Semantic subtyping is an approach to define subtyping relations for type systems featuring union and intersection type connectives. It has been studied only for strict languages, and it is unsound for non-strict semantics. In this work, we study how to adapt this approach to non-strict languages: in particular, we define a type system using semantic subtyping for a functional language with a call-by-need semantics. We do so by introducing an explicit representation for divergence in the types, so that the type system distinguishes expressions that are results from those which are computations that might diverge.
Cite as
Tommaso Petrucciani, Giuseppe Castagna, Davide Ancona, and Elena Zucca. Semantic Subtyping for Non-Strict Languages. In 24th International Conference on Types for Proofs and Programs (TYPES 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 130, pp. 4:1-4:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{petrucciani_et_al:LIPIcs.TYPES.2018.4,
author = {Petrucciani, Tommaso and Castagna, Giuseppe and Ancona, Davide and Zucca, Elena},
title = {{Semantic Subtyping for Non-Strict Languages}},
booktitle = {24th International Conference on Types for Proofs and Programs (TYPES 2018)},
pages = {4:1--4:24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-106-1},
ISSN = {1868-8969},
year = {2019},
volume = {130},
editor = {Dybjer, Peter and Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2018.4},
URN = {urn:nbn:de:0030-drops-114083},
doi = {10.4230/LIPIcs.TYPES.2018.4},
annote = {Keywords: Semantic subtyping, non-strict semantics, call-by-need, union types, intersection types}
}
Document
New Formalized Results on the Meta-Theory of a Paraconsistent Logic
Abstract
Classical logics are explosive, meaning that everything follows from a contradiction. Paraconsistent logics are logics that are not explosive. This paper presents the meta-theory of a paraconsistent infinite-valued logic, in particular new results showing that while the question of validity for a given formula can be reduced to a consideration of only finitely many truth values, this does not mean that the logic collapses to a finite-valued logic. All definitions and theorems are formalized in the Isabelle/HOL proof assistant.
Cite as
Anders Schlichtkrull. New Formalized Results on the Meta-Theory of a Paraconsistent Logic. In 24th International Conference on Types for Proofs and Programs (TYPES 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 130, pp. 5:1-5:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{schlichtkrull:LIPIcs.TYPES.2018.5,
author = {Schlichtkrull, Anders},
title = {{New Formalized Results on the Meta-Theory of a Paraconsistent Logic}},
booktitle = {24th International Conference on Types for Proofs and Programs (TYPES 2018)},
pages = {5:1--5:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-106-1},
ISSN = {1868-8969},
year = {2019},
volume = {130},
editor = {Dybjer, Peter and Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2018.5},
URN = {urn:nbn:de:0030-drops-114098},
doi = {10.4230/LIPIcs.TYPES.2018.5},
annote = {Keywords: Paraconsistent logic, Many-valued logic, Formalization, Isabelle proof assistant, Paraconsistency}
}
Document
Normalization by Evaluation for Typed Weak lambda-Reduction
Abstract
Weak reduction relations in the lambda-calculus are characterized by the rejection of the so-called xi-rule, which allows arbitrary reductions under abstractions. A notable instance of weak reduction can be found in the literature under the name restricted reduction or weak lambda-reduction.
In this work, we attack the problem of algorithmically computing normal forms for lambda-wk, the lambda-calculus with weak lambda-reduction. We do so by first contrasting it with other weak systems, arguing that their notion of reduction is not strong enough to compute lambda-wk-normal forms. We observe that some aspects of weak lambda-reduction prevent us from normalizing lambda-wk directly, thus devise a new, better-behaved weak calculus lambda-ex, and reduce the normalization problem for lambda-w to that of lambda-ex. We finally define type systems for both calculi and apply Normalization by Evaluation to lambda-ex, obtaining a normalization proof for lambda-wk as a corollary. We formalize all our results in Agda, a proof-assistant based on intensional Martin-Löf Type Theory.
Cite as
Filippo Sestini. Normalization by Evaluation for Typed Weak lambda-Reduction. In 24th International Conference on Types for Proofs and Programs (TYPES 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 130, pp. 6:1-6:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{sestini:LIPIcs.TYPES.2018.6,
author = {Sestini, Filippo},
title = {{Normalization by Evaluation for Typed Weak lambda-Reduction}},
booktitle = {24th International Conference on Types for Proofs and Programs (TYPES 2018)},
pages = {6:1--6:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-106-1},
ISSN = {1868-8969},
year = {2019},
volume = {130},
editor = {Dybjer, Peter and Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2018.6},
URN = {urn:nbn:de:0030-drops-114101},
doi = {10.4230/LIPIcs.TYPES.2018.6},
annote = {Keywords: normalization, lambda-calculus, reduction, term-rewriting, Agda}
}
Document
Cubical Assemblies, a Univalent and Impredicative Universe and a Failure of Propositional Resizing
Abstract
We construct a model of cubical type theory with a univalent and impredicative universe in a category of cubical assemblies. We show that this impredicative universe in the cubical assembly model does not satisfy a form of propositional resizing.
Cite as
Taichi Uemura. Cubical Assemblies, a Univalent and Impredicative Universe and a Failure of Propositional Resizing. In 24th International Conference on Types for Proofs and Programs (TYPES 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 130, pp. 7:1-7:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{uemura:LIPIcs.TYPES.2018.7,
author = {Uemura, Taichi},
title = {{Cubical Assemblies, a Univalent and Impredicative Universe and a Failure of Propositional Resizing}},
booktitle = {24th International Conference on Types for Proofs and Programs (TYPES 2018)},
pages = {7:1--7:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-106-1},
ISSN = {1868-8969},
year = {2019},
volume = {130},
editor = {Dybjer, Peter and Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2018.7},
URN = {urn:nbn:de:0030-drops-114118},
doi = {10.4230/LIPIcs.TYPES.2018.7},
annote = {Keywords: Cubical type theory, Realizability, Impredicative universe, Univalence, Propositional resizing}
}