Parameter-passing and the lambda calculus

The choice of a parameter-passing technique is an important decision in the design of a high-level programming language. To clarify some of the semantic aspects of the decision, we develop, analyze, and compare modifications of the $\lambda$-calculus for the most common parameter-passing techniques. More specifically, for each parameter-passing technique we provide (1) a program rewriting semantics for a language with side-effects and first-class procedures based on the respective parameter-passing technique; (2) an equational theory derived from the rewriting semantics; (3) a formal analysis of the correspondence between the calculus and the semantics; and (4) a strong normalization theorem for the largest possible imperative fragment of the theory. A comparison of the various systems reveals that Algol's call-by-name indeed satisfies the well-known $\beta$ rule of the original $\lambda$-calculus, but at the cost of complicated axioms for the imperative part of the theory. The simplest and most appealing axiom system appears to be the one for a call-by-value language with reference cells as first-class values