University of Birmingham > Talks@bham > Theoretical computer science seminar > The Dialectica models of type theory

## The Dialectica models of type theoryAdd to your list(s) Download to your calendar using vCal - Sean Moss (Oxford, formerly Cambridge)
- Friday 09 February 2018, 11:00-12:00
- 217, School of Computer Science.
If you have a question about this talk, please contact Paul Taylor. room 217, not Sloman Lounge Gödel’s Dialectica interpretation was used to prove the consistency of Heyting arithmetic relative to a quantifier-free theory of computable functionals. Following de Paiva’s work on Dialectica categories, we can understand the interpretation as arising from the emergent structure on a certain ‘Dialectica category’, built out of some base category of types. I will show how this ‘Dialectica construction’, along with others such as that based on the variant of Dialectica due to Diller and Nahm, can be generalized to the dependently-typed setting using a logical predicates style theory for display map categories. This talk is part of the Theoretical computer science seminar series. ## This talk is included in these lists:- 217, School of Computer Science
- Computer Science Departmental Series
- Computer Science Distinguished Seminars
- Theoretical computer science seminar
- computer sience
Note that ex-directory lists are not shown. |
## Other listsCombinatorics and Probability seminar Analysis Reading Seminar 2019/2020 dddd## Other talksControl variates for computing transport coefficients TBA TBA Ultrafast Spectroscopy and Microscopy as probes of Energy Materials TBC Life : it’s out there, but what and why ? |