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