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 listsPIPS - Postgraduate Informal Physics Seminars Speech Recognition by Synthesis Seminars Analysis seminar## Other talksThe development of an optically pumped magnetometer based MEG system When less is more - reduced physics simulations of the solar wind Ultrafast, all-optical, and highly efficient imaging of molecular chirality Hodge Theory: Connecting Algebra and Analysis Provably Convergent Plug-and-Play Quasi-Newton Methods for Imaging Inverse Problems Sensing and metrology activities at NPL, India |