University of Birmingham > Talks@bham > Theoretical computer science seminar > Type Theory in Type Theory using Quotient Inductive Types

## Type Theory in Type Theory using Quotient Inductive TypesAdd to your list(s) Download to your calendar using vCal - Ambrus Kaposi (Nottingham)
- Friday 26 February 2016, 11:00-12:00
- Computer Science, The Sloman Lounge (UG).
If you have a question about this talk, please contact Neel Krishnaswami. We present an internal formalisation of a type heory with dependent types in Type Theory using a special case of higher inductive types from Homotopy Type Theory which we call quotient inductive types (QITs). Our formalisation of type theory avoids referring to preterms or a typability relation but defines directly well typed objects by an inductive definition. We use the elimination principle to define the set-theoretic and logical predicate interpretation. The work has been formalized using the Agda system extended with QITs using postulates. This talk is part of the Theoretical computer science seminar series. ## This talk is included in these lists:- Computer Science Departmental Series
- Computer Science Distinguished Seminars
- Computer Science, The Sloman Lounge (UG)
- Theoretical computer science seminar
Note that ex-directory lists are not shown. |
## Other listsParticle Physics Seminars Applied Mathematics Seminar Series School of Chemistry Seminars## Other talksQuantum simulation of strongly correlated fermions: A theory perspective LovĂˇsz' Theorem and Comonads in Finite Model Theory Generalised hydrodynamics and universalities of transport in integrable (and non-integrable) spin chains |