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 listsType the title of a new list here Test Speech Recognition by Synthesis Seminars## Other talksRSC S F Boys-A Rahman Award Lecture RSC 2019 Dalton Emerging Researcher Award Lecture The Griess Algebra and the Monster Machine Learning with Causal Structure Property Relationship (CSPR): Solubility Prediction in Organic Solvents and Water The Suzuki Chain The Leech Lattice and the Conway Groups |