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
- computer sience
Note that ex-directory lists are not shown. |
## Other listsCold atoms Cold Atoms Nuclear physics seminars## Other talksTBC View fusion vis-à-vis a Bayesian interpretation of Black-Litterman for portfolio allocation Advancing biomedical photoacoustic imaging using structured light and optical microresonators [Colloquium:] Aperture Fever: The Extremely Large Telescope The science of the large scale heliosphere and the missions that made it possible |