G. Jacopini et G. Sontacchi, GENERAL RECURSIVE FUNCTIONS IN A VERY SIMPLY INTERPRETABLE TYPED LAMBDA-CALCULUS, Theoretical computer science, 121(1-2), 1993, pp. 169-178
In this paper we add to the usual typed lambda-calculus four constants
(DELTA, OMEGA, rho, theta) and two reduction rules (delta, omega). Th
is language combines the simplicity of interpretation of the usual typ
ed lambda-calculus and the universatity of the untyped lambda-calculus
. We prove, in fact, that each partial recursive function is represent
able in this language.