## A realizability model for a type theory

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