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

The Dialectica models of type theory

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on from the University of Cambridge.