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
Times are displayed in time zone: (GMT+01:00) Greenwich Mean Time : Belfast change

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