books-programmingLanguagesNotesToSelf

on total functions:

" Girard and Reynolds’ System F (1971): characterization of the provably total functions of second- order arithmetic Coquand’s Calculus of Constructions (1984): extending system F into an hybrid formalism for both proofs and programs (consistency = termination of evaluation) "

"

    Within each of the two paradigms there are several versions of typed lambda calculus. In many important systems, especially those a la Church, it is the case that terms that do have a type always possess a normal form. By the unsolvability of the halting problem this implies that not all computable functions can be represented by a typed term, see Barendregt (1990), Theorem 4.2.15. This is not so bad as it sounds, because in order to find such computable functions that cannot be represented, one has to stand on one's head. For example in 2, the second order typed lambda calculus, only those partial recursive functions cannot be represented that happen to be total, but not provably so in mathematical analysis (second order arithmetic).

"