The lambda calculus and its relation to programming languages
Arthur Evans · 1972
An approach to the formal specification of the semantics of the programming language PAL is presented. A subset of the language is exhibited which is equivalent to Church's λ -calculus, and the semantics of that subset is specified by transformation rules from it to the λ -calculus. The semantics of the basic operators of the language (such as “?rdquo;) is defined by axiomatization. The remainder of the language is specified by exhibiting an interpretor for it, the interpretor being expressed in the subset. The approach is tutorial in nature, concentrating on explaining the methods rather than on giving the details. No knowledge of the λ -calculus is assumed.