In any model of typed λ–calculus contaning
some basic arithmetic, a functional p→e (pro-
cedure →expression) will be defined which in-
verts the evaluation functional for typed λ–
terms. Combined with the evaluation func-
tional, p→e yields an efficient normalization
algorithm. The method is extended to λ–
calculi with constants and is used to normalize
(the λ–representations of) natural deduction
proofs of (higher order) arithmetic. A conse-
quence of theoretical interest is a strong com-
pleteness theorem for βη–reduction, generaliz-
ing results of Friedman [?] and Statman [?]:
If two λ–terms have the same value in some
model containing representations of the prim-
itive recursive functions (of level 1) then they
are provably equal in the βη–calculus.