The \(\lambda \mu^{\mathbf{T}}\)-calculus (Q1946673)

The calculus \(\lambda\mu^{\mathbf{T}}\), a combination of Parigot's \(\lambda\mu\)-calculus and Gödel's \textbf{T}, is introduced. The motivation is to provide a type-theoretic framework for challenge constructs in real programming languages, including datatypes such as the natural numbers, primitive recursion, and control operators such as catch and throw. In other words, the paper aims at a synthesis of classical computation with datatypes with a conventional metatheory of typing and reduction. Meta-theoretical properties of \(\lambda\mu^{\mathbf{T}}\), such as subject reduction, normal forms, confluence and strong normalization, are studied. For the proofs of the latter two properties some adaptations of known techniques from the literature are required. Moreover, it is shown that exactly the provably recursive functions in first-order arithmetic can be represented in \(\lambda\mu^{\mathbf{T}}\).