Loïc Pujet: Church's Thesis in Type Theory

Abstract

The internal Church Thesis states that all integer functions are computable by Turing Machines. Together with Markov's principle, it is one of the defining principles of the Russian school of constructive mathematics.

This might not sound very surprising to a type theorist: after all, in Martin-Löf's Type Theory, functions *already* are programs. Thus, one may internalise Church's Thesis by extending the language with a "quote" operator that reifies the code of functions. However, although this strategy is quite natural from a programming perspective, the existence of quote has surprising consequences on the logic, and it is not clear the the resulting system is consistent.

In this talk, I will discuss some of the consequences of Church Thesis in Martin-Löf's type theory, and I will go over Pédrot's recent proof of consistency.