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

  Browse A-Z

Log in

System Admin (disabled)details Birmingham usersdetails No account?details

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

Type Theory in Type Theory using Quotient Inductive Types

Add 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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

Other lists

PIPS - Postgraduate Informal Physics Seminars Speech Recognition by Synthesis Seminars Analysis seminar

Other talks

The 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
 

Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on talks.cam from the University of Cambridge.