Volume
LIPIcs, Volume 175
25th International Conference on Types for Proofs and Programs (TYPES 2019)
Event
TYPES 2019, June 11-14, 2019, Oslo, NorwayEditors
Publication Details
- published at: 2020-09-24
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-158-0
- DBLP: db/conf/types/types2019
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 175, TYPES 2019, Complete Volume
Abstract
LIPIcs, Volume 175, TYPES 2019, Complete Volume
Cite as
25th International Conference on Types for Proofs and Programs (TYPES 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 175, pp. 1-256, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@Proceedings{bezem_et_al:LIPIcs.TYPES.2019,
title = {{LIPIcs, Volume 175, TYPES 2019, Complete Volume}},
booktitle = {25th International Conference on Types for Proofs and Programs (TYPES 2019)},
pages = {1--256},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-158-0},
ISSN = {1868-8969},
year = {2020},
volume = {175},
editor = {Bezem, Marc and Mahboubi, Assia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2019},
URN = {urn:nbn:de:0030-drops-130639},
doi = {10.4230/LIPIcs.TYPES.2019},
annote = {Keywords: LIPIcs, Volume 175, TYPES 2019, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
25th International Conference on Types for Proofs and Programs (TYPES 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 175, pp. 0:i-0:x, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{bezem_et_al:LIPIcs.TYPES.2019.0,
author = {Bezem, Marc and Mahboubi, Assia},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {25th International Conference on Types for Proofs and Programs (TYPES 2019)},
pages = {0:i--0:x},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-158-0},
ISSN = {1868-8969},
year = {2020},
volume = {175},
editor = {Bezem, Marc and Mahboubi, Assia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2019.0},
URN = {urn:nbn:de:0030-drops-130640},
doi = {10.4230/LIPIcs.TYPES.2019.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Making Isabelle Content Accessible in Knowledge Representation Formats
Abstract
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.
Cite as
Michael Kohlhase, Florian Rabe, and Makarius Wenzel. Making Isabelle Content Accessible in Knowledge Representation Formats. In 25th International Conference on Types for Proofs and Programs (TYPES 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 175, pp. 1:1-1:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{kohlhase_et_al:LIPIcs.TYPES.2019.1,
author = {Kohlhase, Michael and Rabe, Florian and Wenzel, Makarius},
title = {{Making Isabelle Content Accessible in Knowledge Representation Formats}},
booktitle = {25th International Conference on Types for Proofs and Programs (TYPES 2019)},
pages = {1:1--1:24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-158-0},
ISSN = {1868-8969},
year = {2020},
volume = {175},
editor = {Bezem, Marc and Mahboubi, Assia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2019.1},
URN = {urn:nbn:de:0030-drops-130651},
doi = {10.4230/LIPIcs.TYPES.2019.1},
annote = {Keywords: Isabelle, PIDE, OMDoc, MMT, library, export}
}
Document
Type Theory Unchained: Extending Agda with User-Defined Rewrite Rules
Abstract
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.
Cite as
Jesper Cockx. Type Theory Unchained: Extending Agda with User-Defined Rewrite Rules. In 25th International Conference on Types for Proofs and Programs (TYPES 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 175, pp. 2:1-2:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{cockx:LIPIcs.TYPES.2019.2,
author = {Cockx, Jesper},
title = {{Type Theory Unchained: Extending Agda with User-Defined Rewrite Rules}},
booktitle = {25th International Conference on Types for Proofs and Programs (TYPES 2019)},
pages = {2:1--2:27},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-158-0},
ISSN = {1868-8969},
year = {2020},
volume = {175},
editor = {Bezem, Marc and Mahboubi, Assia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2019.2},
URN = {urn:nbn:de:0030-drops-130666},
doi = {10.4230/LIPIcs.TYPES.2019.2},
annote = {Keywords: Dependent types, Proof assistants, Rewrite rules, Higher-order rewriting, Agda}
}
Document
A Quantitative Understanding of Pattern Matching
Abstract
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.
Cite as
Sandra Alves, Delia Kesner, and Daniel Ventura. A Quantitative Understanding of Pattern Matching. In 25th International Conference on Types for Proofs and Programs (TYPES 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 175, pp. 3:1-3:36, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{alves_et_al:LIPIcs.TYPES.2019.3,
author = {Alves, Sandra and Kesner, Delia and Ventura, Daniel},
title = {{A Quantitative Understanding of Pattern Matching}},
booktitle = {25th International Conference on Types for Proofs and Programs (TYPES 2019)},
pages = {3:1--3:36},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-158-0},
ISSN = {1868-8969},
year = {2020},
volume = {175},
editor = {Bezem, Marc and Mahboubi, Assia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2019.3},
URN = {urn:nbn:de:0030-drops-130672},
doi = {10.4230/LIPIcs.TYPES.2019.3},
annote = {Keywords: Intersection Types, Pattern Matching, Exact Bounds}
}
Document
Big Step Normalisation for Type Theory
Abstract
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.
Cite as
Thorsten Altenkirch and Colin Geniet. Big Step Normalisation for Type Theory. In 25th International Conference on Types for Proofs and Programs (TYPES 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 175, pp. 4:1-4:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{altenkirch_et_al:LIPIcs.TYPES.2019.4,
author = {Altenkirch, Thorsten and Geniet, Colin},
title = {{Big Step Normalisation for Type Theory}},
booktitle = {25th International Conference on Types for Proofs and Programs (TYPES 2019)},
pages = {4:1--4:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-158-0},
ISSN = {1868-8969},
year = {2020},
volume = {175},
editor = {Bezem, Marc and Mahboubi, Assia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2019.4},
URN = {urn:nbn:de:0030-drops-130682},
doi = {10.4230/LIPIcs.TYPES.2019.4},
annote = {Keywords: Normalisation, big step normalisation, type theory, dependent types, Agda}
}
Document
From Cubes to Twisted Cubes via Graph Morphisms in Type Theory
Abstract
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).
Cite as
Gun Pinyo and Nicolai Kraus. From Cubes to Twisted Cubes via Graph Morphisms in Type Theory. In 25th International Conference on Types for Proofs and Programs (TYPES 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 175, pp. 5:1-5:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{pinyo_et_al:LIPIcs.TYPES.2019.5,
author = {Pinyo, Gun and Kraus, Nicolai},
title = {{From Cubes to Twisted Cubes via Graph Morphisms in Type Theory}},
booktitle = {25th International Conference on Types for Proofs and Programs (TYPES 2019)},
pages = {5:1--5:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-158-0},
ISSN = {1868-8969},
year = {2020},
volume = {175},
editor = {Bezem, Marc and Mahboubi, Assia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2019.5},
URN = {urn:nbn:de:0030-drops-130694},
doi = {10.4230/LIPIcs.TYPES.2019.5},
annote = {Keywords: homotopy type theory, cubical sets, directed equality, graph morphisms}
}
Document
For Finitary Induction-Induction, Induction Is Enough
Abstract
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.
Cite as
Ambrus Kaposi, András Kovács, and Ambroise Lafont. For Finitary Induction-Induction, Induction Is Enough. In 25th International Conference on Types for Proofs and Programs (TYPES 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 175, pp. 6:1-6:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{kaposi_et_al:LIPIcs.TYPES.2019.6,
author = {Kaposi, Ambrus and Kov\'{a}cs, Andr\'{a}s and Lafont, Ambroise},
title = {{For Finitary Induction-Induction, Induction Is Enough}},
booktitle = {25th International Conference on Types for Proofs and Programs (TYPES 2019)},
pages = {6:1--6:30},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-158-0},
ISSN = {1868-8969},
year = {2020},
volume = {175},
editor = {Bezem, Marc and Mahboubi, Assia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2019.6},
URN = {urn:nbn:de:0030-drops-130707},
doi = {10.4230/LIPIcs.TYPES.2019.6},
annote = {Keywords: type theory, inductive types, inductive-inductive types}
}
Document
Eta-Equivalence in Core Dependent Haskell
Abstract
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.
Cite as
Anastasiya Kravchuk-Kirilyuk, Antoine Voizard, and Stephanie Weirich. Eta-Equivalence in Core Dependent Haskell. In 25th International Conference on Types for Proofs and Programs (TYPES 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 175, pp. 7:1-7:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{kravchukkirilyuk_et_al:LIPIcs.TYPES.2019.7,
author = {Kravchuk-Kirilyuk, Anastasiya and Voizard, Antoine and Weirich, Stephanie},
title = {{Eta-Equivalence in Core Dependent Haskell}},
booktitle = {25th International Conference on Types for Proofs and Programs (TYPES 2019)},
pages = {7:1--7:31},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-158-0},
ISSN = {1868-8969},
year = {2020},
volume = {175},
editor = {Bezem, Marc and Mahboubi, Assia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2019.7},
URN = {urn:nbn:de:0030-drops-130716},
doi = {10.4230/LIPIcs.TYPES.2019.7},
annote = {Keywords: Dependent types, Haskell, Irrelevance, Eta-equivalence}
}
Document
Coherence for Monoidal Groupoids in HoTT
Abstract
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.
Cite as
Stefano Piceghello. Coherence for Monoidal Groupoids in HoTT. In 25th International Conference on Types for Proofs and Programs (TYPES 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 175, pp. 8:1-8:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{piceghello:LIPIcs.TYPES.2019.8,
author = {Piceghello, Stefano},
title = {{Coherence for Monoidal Groupoids in HoTT}},
booktitle = {25th International Conference on Types for Proofs and Programs (TYPES 2019)},
pages = {8:1--8:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-158-0},
ISSN = {1868-8969},
year = {2020},
volume = {175},
editor = {Bezem, Marc and Mahboubi, Assia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2019.8},
URN = {urn:nbn:de:0030-drops-130722},
doi = {10.4230/LIPIcs.TYPES.2019.8},
annote = {Keywords: homotopy type theory, coherence, monoidal categories, groupoids, higher inductive types, formalisation, Coq}
}
Document
Is Impredicativity Implicitly Implicit?
Abstract
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.
Cite as
Stefan Monnier and Nathaniel Bos. Is Impredicativity Implicitly Implicit?. In 25th International Conference on Types for Proofs and Programs (TYPES 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 175, pp. 9:1-9:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{monnier_et_al:LIPIcs.TYPES.2019.9,
author = {Monnier, Stefan and Bos, Nathaniel},
title = {{Is Impredicativity Implicitly Implicit?}},
booktitle = {25th International Conference on Types for Proofs and Programs (TYPES 2019)},
pages = {9:1--9:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-158-0},
ISSN = {1868-8969},
year = {2020},
volume = {175},
editor = {Bezem, Marc and Mahboubi, Assia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2019.9},
URN = {urn:nbn:de:0030-drops-130730},
doi = {10.4230/LIPIcs.TYPES.2019.9},
annote = {Keywords: Impredicativity, Pure type systems, Inductive types, Erasable arguments, Proof irrelevance, Implicit arguments, Universe polymorphism}
}
Document
Higher Inductive Type Eliminators Without Paths
Abstract
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.
Cite as
Nils Anders Danielsson. Higher Inductive Type Eliminators Without Paths. In 25th International Conference on Types for Proofs and Programs (TYPES 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 175, pp. 10:1-10:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{danielsson:LIPIcs.TYPES.2019.10,
author = {Danielsson, Nils Anders},
title = {{Higher Inductive Type Eliminators Without Paths}},
booktitle = {25th International Conference on Types for Proofs and Programs (TYPES 2019)},
pages = {10:1--10:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-158-0},
ISSN = {1868-8969},
year = {2020},
volume = {175},
editor = {Bezem, Marc and Mahboubi, Assia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2019.10},
URN = {urn:nbn:de:0030-drops-130749},
doi = {10.4230/LIPIcs.TYPES.2019.10},
annote = {Keywords: Cubical Agda, higher inductive types}
}