eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-11-18
130
0
0
10.4230/LIPIcs.TYPES.2018
article
LIPIcs, Volume 130, TYPES'18, Complete Volume
Dybjer, Peter
1
Espírito Santo, José
2
Pinto, Luís
2
Department of Computer Science and Engineering, Chalmers University of Technology, Göteborg, Sweden
Centro de Matemática, Universidade do Minho, Braga, Portugal
LIPIcs, Volume 130, TYPES'18, Complete Volume
https://drops.dagstuhl.de/storage/00lipics/lipics-vol130-types2018/LIPIcs.TYPES.2018/LIPIcs.TYPES.2018.pdf
Theory of computation,Type theory; Constructive mathematics; Logic and verification; Program verification, Software and its engineering
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-11-18
130
0:i
0:x
10.4230/LIPIcs.TYPES.2018.0
article
Front Matter, Table of Contents, Preface, Conference Organization
Dybjer, Peter
1
Espírito Santo, José
2
Pinto, Luís
2
Department of Computer Science and Engineering, Chalmers University of Technology, Göteborg, Sweden
Centro de Matemática, Universidade do Minho, Braga, Portugal
Front Matter, Table of Contents, Preface, Conference Organization
https://drops.dagstuhl.de/storage/00lipics/lipics-vol130-types2018/LIPIcs.TYPES.2018.0/LIPIcs.TYPES.2018.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-11-18
130
1:1
1:22
10.4230/LIPIcs.TYPES.2018.1
article
Martin Hofmann’s Case for Non-Strictly Positive Data Types
Berger, Ulrich
1
https://orcid.org/0000-0002-7677-3582
Matthes, Ralph
2
https://orcid.org/0000-0002-7299-2411
Setzer, Anton
1
https://orcid.org/0000-0001-5322-6060
Dept. of Computer Science, Swansea University, United Kingdom
IRIT (CNRS and University of Toulouse), France
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol130-types2018/LIPIcs.TYPES.2018.1/LIPIcs.TYPES.2018.1.pdf
non strictly-positive data types
breadth-first traversal
program verification
Mendler-style recursion
System F
theorem proving
Coq
Agda
Haskell
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-11-18
130
2:1
2:11
10.4230/LIPIcs.TYPES.2018.2
article
A Simpler Undecidability Proof for System F Inhabitation
Dudenhefner, Andrej
1
Rehof, Jakob
1
Technical University of Dortmund, Dortmund, Germany
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".
https://drops.dagstuhl.de/storage/00lipics/lipics-vol130-types2018/LIPIcs.TYPES.2018.2/LIPIcs.TYPES.2018.2.pdf
System F
Lambda Calculus
Inhabitation
Propositional Logic
Provability
Undecidability
Coq
Formalization
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-11-18
130
3:1
3:21
10.4230/LIPIcs.TYPES.2018.3
article
Dependent Sums and Dependent Products in Bishop’s Set Theory
Petrakis, Iosif
1
https://orcid.org/0000-0002-4121-7455
Ludwig-Maximilians-Universität Munich, Theresienstrasse 39, Germany
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol130-types2018/LIPIcs.TYPES.2018.3/LIPIcs.TYPES.2018.3.pdf
Bishop’s constructive mathematics
Martin-Löf’s type theory
dependent sums
dependent products
type-theoretic axiom of choice
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-11-18
130
4:1
4:24
10.4230/LIPIcs.TYPES.2018.4
article
Semantic Subtyping for Non-Strict Languages
Petrucciani, Tommaso
1
2
Castagna, Giuseppe
3
Ancona, Davide
1
Zucca, Elena
1
DIBRIS, Università di Genova, Italy
IRIF, Université Paris Diderot, France
CNRS, IRIF, Université Paris Diderot, France
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol130-types2018/LIPIcs.TYPES.2018.4/LIPIcs.TYPES.2018.4.pdf
Semantic subtyping
non-strict semantics
call-by-need
union types
intersection types
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-11-18
130
5:1
5:15
10.4230/LIPIcs.TYPES.2018.5
article
New Formalized Results on the Meta-Theory of a Paraconsistent Logic
Schlichtkrull, Anders
1
https://orcid.org/0000-0001-9212-6150
DTU Compute - Department of Applied Mathematics and Computer Science, Technical University of Denmark, Richard Petersens Plads, Building 324, DK-2800 Kongens Lyngby, Denmark
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol130-types2018/LIPIcs.TYPES.2018.5/LIPIcs.TYPES.2018.5.pdf
Paraconsistent logic
Many-valued logic
Formalization
Isabelle proof assistant
Paraconsistency
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-11-18
130
6:1
6:17
10.4230/LIPIcs.TYPES.2018.6
article
Normalization by Evaluation for Typed Weak lambda-Reduction
Sestini, Filippo
1
Functional Programming Laboratory, University of Nottingham, United Kingdom
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol130-types2018/LIPIcs.TYPES.2018.6/LIPIcs.TYPES.2018.6.pdf
normalization
lambda-calculus
reduction
term-rewriting
Agda
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-11-18
130
7:1
7:20
10.4230/LIPIcs.TYPES.2018.7
article
Cubical Assemblies, a Univalent and Impredicative Universe and a Failure of Propositional Resizing
Uemura, Taichi
1
https://orcid.org/0000-0003-4930-1384
University of Amsterdam, Amsterdam, The Netherlands
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol130-types2018/LIPIcs.TYPES.2018.7/LIPIcs.TYPES.2018.7.pdf
Cubical type theory
Realizability
Impredicative universe
Univalence
Propositional resizing