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 listsMaterialWell Topology and Dynamics Seminar Nanoscale Physics Seminars## Other talksHodge Theory: Connecting Algebra and Analysis The development of an optically pumped magnetometer based MEG system Perfect matchings in random sparsifications of Dirac hypergraphs Provably Convergent Plug-and-Play Quasi-Newton Methods for Imaging Inverse Problems Sensing and metrology activities at NPL, India Modelling uncertainty in image analysis. |