Friday 1 December 2023, 15:30, room 3U47: "A quote? In *my* type theory?", Pierre-Marie Pédrot (Gallinette, Inria Rennes, LS2N).

The internal Church thesis is the statement that all functions ℕ → ℕ are provably computable from within the ambient theory. This principle has been used thoroughly by the Russian constructivist school and is in particular known to be consistent with e.g. simple type theory. Weirdly enough, its status in MLTT is still debated as some experts expect it to be obviously inconsistent and the literature is not extremely engaging. We spearhead the opposite stance, namely that it is a trivial fact. This is justified by an extension of MLTT with quoting primitives, whose consistency and strong normalization are proved through a model based on logical relations which has been partially mechanized in Coq.