Cornell University
Library
Cornell UniversityLibrary

eCommons

Help
Log In(current)
  1. Home
  2. Cornell Computing and Information Science
  3. Computer Science
  4. Computer Science Technical Reports
  5. Programming Language Semantics Using Extensional $\lambda$-Calculus Models

Programming Language Semantics Using Extensional $\lambda$-Calculus Models

File(s)
74-206.ps (452.84 KB)
74-206.pdf (1.22 MB)
Permanent Link(s)
https://hdl.handle.net/1813/6046
Collections
Computer Science Technical Reports
Author
Egli, Herbert
Abstract

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 [6] 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" [12] (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.

Date Issued
1974-04
Publisher
Cornell University
Keywords
computer science
•
technical report
Previously Published as
http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR74-206
Type
technical report

Site Statistics | Help

About eCommons | Policies | Terms of use | Contact Us

copyright © 2002-2026 Cornell University Library | Privacy | Web Accessibility Assistance