Programming Language Semantics Using Extensional $\lambda$-Calculus Models
We prove a theorem which provides an intuitive understanding of the meaning of $\lambda$-terms in Scott's extensional $\lambda$-calculus models. This allows us to use those models for the definition of high-level programming languages. In order to illustrate this we define a programming language which includes blocks and (arbitrary recursive) procedures. Two aspects justify this approach. First of all, the logical properties of those (typeless) $\lambda$-calculus models are appealing for a formalization similar to LCF  which formalizes typed $\lambda$-calculus models. Secondly, not having the type restrictions that LCF imposes allows us to define the semantics of high-level programming languages in the spirit of "mathematical semantics"  (which is usually based on recursively defined domains), thus the semantic nature of syntactic constructs can be exhibited clearly. Keywords: Mathematical semantics, Programming Languages, $\lambda$-calculus Models, typed, typeless, extensional, Logic, LCF.
computer science; technical report
Previously Published As