A realizability model for a type theory

Keiko Nakata

Institute of Cybernetics at TUT

Thursday, 6 November 2014, 14:00
Cybernetica Bldg (Akadeemia tee 21), room B101

Abstract: I will talk about a construction of a domain model for a Martin-Löf dependent type theory based on an extension of the untyped lambda calculus. The domain model naturally gives rise to a realizability model, where the terms of the extended lambda calculus are the realizers. We use the realizability interpretation to prove that both Markov's principle and the undecidablity of the halting problem can be consistently added to the type theory.

(Joint work with Marc Bezem and Thierry Coquand.)

Tarmo Uustalu
Last update 29 October 2014