Definability in Dependent Type Theory

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

• Cory Knapp
• Friday 07 August 2015, 13:00-14:00
• CS 217.

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.

This talk is included in these lists:

• CS 217
• Lab Lunch

Note that ex-directory lists are not shown.