University of Birmingham > Talks@bham > Lab Lunch > Definability in Dependent Type Theory

Definability in Dependent Type Theory

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Uday Reddy.

Definability is a central question in both classical model theory (where we are interested in subsets of a model defined by a formula) and for simply-typed theories (where we are interested in elements of a model defined by a term); however, the question of definability for dependent type theory (MLTT specifically) seems neglected. I will present a sketch of a program to begin studying definability for MLTT , structured around the question “Are all MLTT definable functions (N->N)->N continuous?” The general theory should also have connections to normalization by evaluation and other meta-theoretic questions about Martin-L f type theory.

This talk is part of the Lab Lunch series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


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