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

Quotient inductive-inductive types (QIITs) generalise inductive types in two ways: a QIIT can have more than one sort and the later sorts can be indexed over the previous ones. In addition, equality constructors are also allowed. We work in a setting with uniqueness of identity proofs, hence we use the term QIIT instead of higher inductive-inductive type. An example of a QIIT is the well-typed (intrinsic) syntax of type theory quotiented by conversion. In this paper first we specify finitary QIITs using a domain-specific type theory which we call the theory of signatures. The syntax of the theory of signatures is given by a QIIT as well. Then, using this syntax we show that all specified QIITs exist and they have a dependent elimination principle. We also show that algebras of a signature form a category with families (CwF) and use the internal language of this CwF to show that dependent elimination is equivalent to initiality.

Slides (prez.pdf)90KiB

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