A Caltech Library Service

Lambda Logic

Rudin, Leonid (1981) Lambda Logic. California Institute of Technology . (Unpublished)

See Usage Policy.

Other (Adobe PDF (2.4MB))
See Usage Policy.


Use this Persistent URL to link to this item:


The main aim of this paper is to formulate "natural" logical foundations for type-free lambda-calculus. The importance of such foundations for analyzing arbitrary order computational properties of programs is emphasized. Lamda logic is a deductive system based on combinatory lambda-terms. Its language is conceived by extending the set of lambda-terms through the addition of new terms which are logical connectives. The model for lamda-logic is Dana Scott's D infinity, which can be represented as a pseudo-Boolean algebra. We present detailed proof that D infinity can be constructed as a Heyting algebra, thus being a model for some Heyting intuitionistic logical system. Our result, briefly described above, poses new problems. In particular, the relation between algebraic models of computer languages and the algebraic model theory is of great interest if one wants to establish a logical framework for the verification of programs written in these languages.

Item Type:Report or Paper (Technical Report)
Group:Computer Science Technical Reports
Record Number:CaltechCSTR:1981.4521-tr-81
Persistent URL:
Usage Policy:You are granted permission for individual, educational, research and non-commercial reproduction, distribution, display and performance of this work in any format.
ID Code:27052
Deposited By: Imported from CaltechCSTR
Deposited On:02 Jan 2003
Last Modified:03 Oct 2019 03:20

Repository Staff Only: item control page