Lambda Logic

Rudin, Leonid (1981) Lambda Logic. Technical Report. California Institute of Technology. [CaltechCSTR:1981.4521-tr-81]

Full text available as:

	Postscript - Requires a viewer, such as GhostView
	Other (Adobe PDF (2.4MB))

Abstract

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.

EPrint Type:	Monograph (Technical Report)
Subjects:	All Records
ID Code:	473
Deposited By:	Caltech Library System
Deposited On:	02 January 2003
Record Number:	CaltechCSTR:1981.4521-tr-81
Official Persistent URL:	http://resolver.caltech.edu/CaltechCSTR:1981.4521-tr-81
Usage Policy:	You are granted permission for individual, educational, research and non-commercial reproduction, distribution, display and performance of this work in any format.

Archive Staff Only: edit this record