Accession Number:

AD0683394

Title:

LAMBDA-CALCULUS MODELS OF PROGRAMMING LANGUAGES.

Descriptive Note:

Doctoral thesis,

Corporate Author:

MASSACHUSETTS INST OF TECH CAMBRIDGE PROJECT MAC

Personal Author(s):

Report Date:

1968-12-01

Pagination or Media Count:

135.0

Abstract:

Two aspects of programming languages, recursive definitions and type declarations are analyzed in detail, using Churchs lambda-calculus as the programming language model. The main result on recursion is an analogue to Kleenes first recursion theorem If A FA for any lambda-expressions A and F, then A is an extension of YF in the sense that if EYF, any expression containing YF, has a normal form then EYF EA. Y is Currys paradoxical combinator. The result is shown to be invariant for many different versions of Y. A system of types and type declarations is developed for the lambda-calculus and its semantic assumptions are identified. The system is shown to be adequate in the sense that it permits a preprocessor to check formulae prior to evaluation to prevent type errors. It is shown that any formula with a valid assignment of types to all its subexpressions must have a normal form. Author

Subject Categories:

  • Computer Programming and Software
  • Computer Systems

Distribution Statement:

APPROVED FOR PUBLIC RELEASE