Berger, Ulrich and Schwichtenberg, Helmut
An inverse of the evaluation functional for typed Lambda-calculus.
6th Annual IEE Symposium on Logic in Computer Science (LICS'91), 15. - 18. Juli 1991, Amsterdam.
In any model of typed λ-calculus conianing some basic
arithmetic, a functional p - * (procedure—* expression)
will be defined which inverts the evaluation functional
for typed X-terms, Combined with the evaluation
functional, p-e yields an efficient normalization algorithm.
The method is extended to X-calculi with constants
and is used to normalize (the X-representations
of) natural deduction proofs of (higher order) arithmetic.
A consequence of theoretical interest is a strong
completeness theorem for βη-reduction, generalizing
results of Friedman  and Statman [31: If two Xterms
have the same value in some model containing
representations of the primitive recursive functions
(of level 1) then they are provably equal in the βη-