![]() |
![]() |
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
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:
Note that ex-directory lists are not shown. |
Other listsPIPS - Postgraduate Informal Physics Seminars Speech Recognition by Synthesis Seminars Analysis seminarOther 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 |