eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2020-09-24
175
1
256
10.4230/LIPIcs.TYPES.2019
article
LIPIcs, Volume 175, TYPES 2019, Complete Volume
Bezem, Marc
1
Mahboubi, Assia
2
3
University of Bergen, Norway
Inria, Nantes, France
Vrije Universiteit Amsterdam, The Netherlands
LIPIcs, Volume 175, TYPES 2019, Complete Volume
https://drops.dagstuhl.de/storage/00lipics/lipics-vol175-types2019/LIPIcs.TYPES.2019/LIPIcs.TYPES.2019.pdf
LIPIcs, Volume 175, TYPES 2019, Complete Volume
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2020-09-24
175
0:i
0:x
10.4230/LIPIcs.TYPES.2019.0
article
Front Matter, Table of Contents, Preface, Conference Organization
Bezem, Marc
1
Mahboubi, Assia
2
3
University of Bergen, Norway
Inria, Nantes, France
Vrije Universiteit Amsterdam, The Netherlands
Front Matter, Table of Contents, Preface, Conference Organization
https://drops.dagstuhl.de/storage/00lipics/lipics-vol175-types2019/LIPIcs.TYPES.2019.0/LIPIcs.TYPES.2019.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
2020-09-24
175
1:1
1:24
10.4230/LIPIcs.TYPES.2019.1
article
Making Isabelle Content Accessible in Knowledge Representation Formats
Kohlhase, Michael
1
https://orcid.org/0000-0002-9859-6337
Rabe, Florian
1
Wenzel, Makarius
2
University Erlangen-Nürnberg, Germany
Selfemployed, Augsburg, Germany
The libraries of proof assistants like Isabelle, Coq, HOL are notoriously difficult to interpret by external tools: de facto, only the prover itself can parse and process them adequately. In the case of Isabelle, an export of the library into a FAIR (Findable, Accessible, Interoperable, and Reusable) knowledge exchange format was already envisioned by the authors in 1999 but had previously proved too difficult.
After substantial improvements of the Isabelle Prover IDE (PIDE) and the OMDoc/Mmt format since then, we are now able to deliver such an export. Concretely we present an integration of PIDE and Mmt that allows exporting all Isabelle libraries in OMDoc format. Our export covers the full Isabelle distribution and the Archive of Formal Proofs (AFP) - more than 12 thousand theories and locales resulting in over 65 GB of OMDoc/XML.
Such a systematic export of Isabelle content to a well-defined interchange format like OMDoc enables many applications such as dependency management, independent proof checking, or library search.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol175-types2019/LIPIcs.TYPES.2019.1/LIPIcs.TYPES.2019.1.pdf
Isabelle
PIDE
OMDoc
MMT
library
export
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2020-09-24
175
2:1
2:27
10.4230/LIPIcs.TYPES.2019.2
article
Type Theory Unchained: Extending Agda with User-Defined Rewrite Rules
Cockx, Jesper
1
https://orcid.org/0000-0003-3862-4073
Department of Software Technology, TU Delft, The Netherlands
Dependently typed languages such as Coq and Agda can statically guarantee the correctness of our proofs and programs. To provide this guarantee, they restrict users to certain schemes - such as strictly positive datatypes, complete case analysis, and well-founded induction - that are known to be safe. However, these restrictions can be too strict, making programs and proofs harder to write than necessary. On a higher level, they also prevent us from imagining the different ways the language could be extended.
In this paper I show how to extend a dependently typed language with user-defined higher-order non-linear rewrite rules. Rewrite rules are a form of equality reflection that is applied automatically by the typechecker. I have implemented rewrite rules as an extension to Agda, and I give six examples how to use them both to make proofs easier and to experiment with extensions of type theory. I also show how to make rewrite rules interact well with other features of Agda such as η-equality, implicit arguments, data and record types, irrelevance, and universe level polymorphism. Thus rewrite rules break the chains on computation and put its power back into the hands of its rightful owner: yours.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol175-types2019/LIPIcs.TYPES.2019.2/LIPIcs.TYPES.2019.2.pdf
Dependent types
Proof assistants
Rewrite rules
Higher-order rewriting
Agda
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2020-09-24
175
3:1
3:36
10.4230/LIPIcs.TYPES.2019.3
article
A Quantitative Understanding of Pattern Matching
Alves, Sandra
1
Kesner, Delia
2
3
Ventura, Daniel
4
DCC-FCUP & CRACS, University of Porto, Portugal
Université de Paris, CNRS, IRIF, France
Institut Universitaire de France, France
INF, Universidade Federal de Goiás, Goiânia, Brazil
This paper shows that the recent approach to quantitative typing systems for programming languages can be extended to pattern matching features. Indeed, we define two resource-aware type systems, named U and E, for a λ-calculus equipped with pairs for both patterns and terms. Our typing systems borrow some basic ideas from [Antonio Bucciarelli et al., 2015], which characterises (head) normalisation in a qualitative way, in the sense that typability and normalisation coincide. But, in contrast to [Antonio Bucciarelli et al., 2015], our systems also provide quantitative information about the dynamics of the calculus. Indeed, system U provides upper bounds for the length of (head) normalisation sequences plus the size of their corresponding normal forms, while system E, which can be seen as a refinement of system U, produces exact bounds for each of them. This is achieved by means of a non-idempotent intersection type system equipped with different technical tools. First of all, we use product types to type pairs instead of the disjoint unions in [Antonio Bucciarelli et al., 2015], which turn out to be an essential quantitative tool because they remove the confusion between "being a pair" and "being duplicable". Secondly, typing sequents in system E are decorated with tuples of integers, which provide quantitative information about normalisation sequences, notably time (cf. length) and space (cf. size). Moreover, the time resource information is remarkably refined, because it discriminates between different kinds of reduction steps performed during evaluation, so that beta, substitution and matching steps are counted separately. Another key tool of system E is that the type system distinguishes between consuming (contributing to time) and persistent (contributing to space) constructors.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol175-types2019/LIPIcs.TYPES.2019.3/LIPIcs.TYPES.2019.3.pdf
Intersection Types
Pattern Matching
Exact Bounds
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2020-09-24
175
4:1
4:20
10.4230/LIPIcs.TYPES.2019.4
article
Big Step Normalisation for Type Theory
Altenkirch, Thorsten
1
Geniet, Colin
2
https://orcid.org/0000-0003-4034-7634
School for Computer Science, University of Nottingham, UK
Computer Science Department, ENS Paris-Saclay, France
Big step normalisation is a normalisation method for typed lambda-calculi which relies on a purely syntactic recursive evaluator. Termination of that evaluator is proven using a predicate called strong computability, similar to the techniques used to prove strong normalisation of β-reduction for typed lambda-calculi. We generalise big step normalisation to a minimalist dependent type theory. Compared to previous presentations of big step normalisation for e.g. the simply-typed lambda-calculus, we use a quotiented syntax of type theory, which crucially reduces the syntactic complexity introduced by dependent types. Most of the proof has been formalised using Agda.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol175-types2019/LIPIcs.TYPES.2019.4/LIPIcs.TYPES.2019.4.pdf
Normalisation
big step normalisation
type theory
dependent types
Agda
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2020-09-24
175
5:1
5:18
10.4230/LIPIcs.TYPES.2019.5
article
From Cubes to Twisted Cubes via Graph Morphisms in Type Theory
Pinyo, Gun
1
https://orcid.org/0000-0002-8483-5261
Kraus, Nicolai
1
https://orcid.org/0000-0002-8729-4077
School of Computer Science, University of Nottingham, UK
Cube categories are used to encode higher-dimensional categorical structures. They have recently gained significant attention in the community of homotopy type theory and univalent foundations, where types carry the structure of higher groupoids. Bezem, Coquand, and Huber [Bezem et al., 2014] have presented a constructive model of univalence using a specific cube category, which we call the BCH cube category.
The higher categories encoded with the BCH cube category have the property that all morphisms are invertible, mirroring the fact that equality is symmetric. This might not always be desirable: the field of directed type theory considers a notion of equality that is not necessarily invertible.
This motivates us to suggest a category of twisted cubes which avoids built-in invertibility. Our strategy is to first develop several alternative (but equivalent) presentations of the BCH cube category using morphisms between suitably defined graphs. Starting from there, a minor modification allows us to define our category of twisted cubes. We prove several first results about this category, and our work suggests that twisted cubes combine properties of cubes with properties of globes and simplices (tetrahedra).
https://drops.dagstuhl.de/storage/00lipics/lipics-vol175-types2019/LIPIcs.TYPES.2019.5/LIPIcs.TYPES.2019.5.pdf
homotopy type theory
cubical sets
directed equality
graph morphisms
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2020-09-24
175
6:1
6:30
10.4230/LIPIcs.TYPES.2019.6
article
For Finitary Induction-Induction, Induction Is Enough
Kaposi, Ambrus
1
https://orcid.org/0000-0001-9897-8936
Kovács, András
1
https://orcid.org/0000-0002-6375-9781
Lafont, Ambroise
2
https://orcid.org/0000-0002-9299-641X
Eötvös Loránd University, Budapest, Hungary
IMT Atlantique, Inria, LS2N CNRS, Nantes, France
Inductive-inductive types (IITs) are a generalisation of inductive types in type theory. They allow the mutual definition of types with multiple sorts where later sorts can be indexed by previous ones. An example is the Chapman-style syntax of type theory with conversion relations for each sort where e.g. the sort of types is indexed by contexts. In this paper we show that if a model of extensional type theory (ETT) supports indexed W-types, then it supports finitely branching IITs. We use a small internal type theory called the theory of signatures to specify IITs. We show that if a model of ETT supports the syntax for the theory of signatures, then it supports all IITs. We construct this syntax from indexed W-types using preterms and typing relations and prove its initiality following Streicher. The construction of the syntax and its initiality proof were formalised in Agda.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol175-types2019/LIPIcs.TYPES.2019.6/LIPIcs.TYPES.2019.6.pdf
type theory
inductive types
inductive-inductive types
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2020-09-24
175
7:1
7:31
10.4230/LIPIcs.TYPES.2019.7
article
Eta-Equivalence in Core Dependent Haskell
Kravchuk-Kirilyuk, Anastasiya
1
Voizard, Antoine
2
Weirich, Stephanie
2
https://orcid.org/0000-0002-6756-9168
Princeton University, NJ, USA
University of Pennsylvania, Philadelphia, PA, USA
We extend the core semantics for Dependent Haskell with rules for η-equivalence. This semantics is defined by two related calculi, Systems D and DC. The first is a Curry-style dependently-typed language with nontermination, irrelevant arguments, and equality abstraction. The second, inspired by the Glasgow Haskell Compiler’s core language FC, is the explicitly-typed analogue of System D, suitable for implementation in GHC. Our work builds on and extends the existing metatheory for these systems developed using the Coq proof assistant.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol175-types2019/LIPIcs.TYPES.2019.7/LIPIcs.TYPES.2019.7.pdf
Dependent types
Haskell
Irrelevance
Eta-equivalence
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2020-09-24
175
8:1
8:20
10.4230/LIPIcs.TYPES.2019.8
article
Coherence for Monoidal Groupoids in HoTT
Piceghello, Stefano
1
https://orcid.org/0000-0002-4588-4386
Department of Informatics and Department of Mathematics, University of Bergen, Norway
We present a proof of coherence for monoidal groupoids in homotopy type theory. An important role in the formulation and in the proof of coherence is played by groupoids with a free monoidal structure; these can be represented by 1-truncated higher inductive types, with constructors freely generating their defining objects, natural isomorphisms and commutative diagrams. All results included in this paper have been formalised in the proof assistant Coq.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol175-types2019/LIPIcs.TYPES.2019.8/LIPIcs.TYPES.2019.8.pdf
homotopy type theory
coherence
monoidal categories
groupoids
higher inductive types
formalisation
Coq
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2020-09-24
175
9:1
9:19
10.4230/LIPIcs.TYPES.2019.9
article
Is Impredicativity Implicitly Implicit?
Monnier, Stefan
1
https://orcid.org/0000-0001-7597-5273
Bos, Nathaniel
2
Université de Montréal - DIRO, Canada
McGill University - SOCS, Montréal, Canada
Of all the threats to the consistency of a type system, such as side effects and recursion, impredicativity is arguably the least understood. In this paper, we try to investigate it using a kind of blackbox reverse-engineering approach to map the landscape. We look at it with a particular focus on its interaction with the notion of implicit arguments, also known as erasable arguments.
More specifically, we revisit several famous type systems believed to be consistent and which do include some form of impredicativity, and show that they can be refined to equivalent systems where impredicative quantification can be marked as erasable, in a stricter sense than the kind of proof irrelevance notion used for example for Prop terms in systems like Coq.
We hope these observations will lead to a better understanding of why and when impredicativity can be sound. As a first step in this direction, we discuss how these results suggest some extensions of existing systems where constraining impredicativity to erasable quantifications might help preserve consistency.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol175-types2019/LIPIcs.TYPES.2019.9/LIPIcs.TYPES.2019.9.pdf
Impredicativity
Pure type systems
Inductive types
Erasable arguments
Proof irrelevance
Implicit arguments
Universe polymorphism
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2020-09-24
175
10:1
10:18
10.4230/LIPIcs.TYPES.2019.10
article
Higher Inductive Type Eliminators Without Paths
Danielsson, Nils Anders
1
https://orcid.org/0000-0001-8688-0333
University of Gothenburg, Sweden
Cubical Agda has support for higher inductive types. Paths are integral to the working of this feature. However, there are other notions of equality. For instance, Cubical Agda comes with an identity type family for which the J rule computes in the usual way when applied to the canonical proof of reflexivity, whereas typical implementations of the J rule for paths do not.
This text shows how one can use some of the higher inductive types definable in Cubical Agda with arbitrary notions of equality satisfying certain axioms. The method works for several examples taken from the HoTT book, including the interval, the circle, suspensions, pushouts, the propositional truncation, a general truncation operator, and set quotients.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol175-types2019/LIPIcs.TYPES.2019.10/LIPIcs.TYPES.2019.10.pdf
Cubical Agda
higher inductive types