## 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:- CS 217
- Computer Science Departmental Series
- Computer Science Distinguished Seminars
- Lab Lunch
- Theoretical computer science seminar
Note that ex-directory lists are not shown. |
## Other listsAnalysis Seminar Computer Security Seminars Jane Langdale## Other talksLovĂˇsz' Theorem and Comonads in Finite Model Theory Quantum simulation of strongly correlated fermions: A theory perspective Generalised hydrodynamics and universalities of transport in integrable (and non-integrable) spin chains Best Response Dynamics on Random Graphs |