The Dialectica models of type theory

Add 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.