## 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 listsCentre for Computational Biology Seminar Series Cond. Mat. seminar Cold atoms## Other talksRevisiting the relation between subspaces and sublocales RSC 2019 Dalton Emerging Researcher Award Lecture Subgroups of the Monster An attack on ECDSA using lattice techniques Multi-dimensional vector assignment problems (MVA) : Complexity, Approximation and Algorithms Physics at van der Waals interfaces: Twists, incommensurability and emergent phenomena |