## Definability in Dependent Type TheoryAdd 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:Note that ex-directory lists are not shown. |
## Other listsQuantitative Methods in Finance seminar computer sience PIPS - Postgraduate Informal Physics Seminars## Other talksTBA TBA Proofs of Turán's theorem The tragic destiny of Mileva Marić Einstein TBC TBA |