![]() |
![]() |
University of Birmingham > Talks@bham > Theoretical computer science seminar > Constructing Infinitary Quotient-Inductive Types
Constructing Infinitary Quotient-Inductive TypesAdd to your list(s) Download to your calendar using vCal
If you have a question about this talk, please contact Dan Ghica. Quotient-inductive types (QITs) intertwine the inductive construction of data and rules for identifying that data. They are the one-dimensional special case of higher inductive types from Homotopy Type Theory and have been popularised by Altenkirch and his co-authors. At first sight it seems that in constructive type theories QITs are more expressive than the combination of ordinary inductive types with quotient types. This is because they permit infinitary constructs that appear to need the axiom of choice to be modelled using ordinary quotients. However, for a wide class of QITs, called QW-types, with some ingenuity choice can be avoided: these QITs can be expressed using the combination of inductive-inductive definitions, Hofmann-style quotient types, and Abel’s version of size types. The latter, which provide a convenient constructive abstraction of what classically would be accomplished with transfinite ordinals, are used to prove termination of the recursive definitions of the elimination and computation properties of QW-types. The development has been formalised using the Agda theorem-prover and is joint work with Marcelo Fiore and Shaun Steenkamp. This talk is part of the Theoretical computer science seminar series. This talk is included in these lists:
Note that ex-directory lists are not shown. |
Other listsType the title of a new list here SoCS PhD Research Training Sessions Centre for Computational Biology Seminar SeriesOther talksTBA TBA Proofs of Turán's theorem Ultrafast Spectroscopy and Microscopy as probes of Energy Materials An introduction to τ-exceptional sequences Wave turbulence in the Schrödinger-Helmholtz equation |