# 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

# Descriptors:

# Subject Categories:

- Computer Programming and Software
- Computer Systems