Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Fri 18 Jan 2019 11:19 - 11:41 at Sala I - Dependent Types Chair(s): Andreas Abel

Definitional equality—or conversion—for a type theory with a decidable type checking is the simplest tool to prove that two objects are the same, letting the system decide just using computation. Therefore, the more things are equal by conversion, the simpler it is to use a language based on type theory. Proof-irrelevance, stating that any two proofs of the same proposition are equal, is a possible way to extend conversion to make a type theory more powerful. However, this new power comes at a price if we integrate it naively, either by making type checking undecidable or by realizing new axioms—such as uniqueness of identity proofs (UIP)—that are incompatible with other extensions, such as univalence. In this paper, taking inspiration from homotopy type theory, we propose a general way to extend a type theory with definitional proof irrelevance, in a way that keeps type checking decidable and is compatible with univalence. We provide a new criterion to decide whether a proposition can be eliminated over a type (correcting and improving the so-called singleton elimination of Coq) by using techniques coming from recent development on dependent pattern matching without UIP. We show the generality of our approach by providing implementations for both Coq and Agda, both of which are planned to be integrated in future versions of those proof assistants.

slides of the presentation (sprop_popl_19.pdf)4.25MiB

Fri 18 Jan

POPL-2019-Research-Papers
10:35 - 12:03: Research Papers - Dependent Types at Sala I
Chair(s): Andreas AbelGothenburg University
POPL-2019-Research-Papers10:35 - 10:57
Talk
Evan CavalloCarnegie Mellon University, Robert Harper
Link to publication DOI Pre-print File Attached
POPL-2019-Research-Papers10:57 - 11:19
Talk
Thorsten AltenkirchUniversity of Nottingham, Ambrus KaposiUniversity of Nottingham, András KovácsEötvös Loránd University
Link to publication DOI File Attached
POPL-2019-Research-Papers11:19 - 11:41
Talk
Gaetan Gilbert, Jesper CockxChalmers | University of Gothenburg, Matthieu SozeauInria, Nicolas TabareauInria
Link to publication DOI File Attached
POPL-2019-Research-Papers11:41 - 12:03
Talk
Rasmus Ejlers MøgelbergIT University of Copenhagen, Niccolò VeltriIT University of Copenhagen
Link to publication DOI File Attached