Rudin, Leonid (1981) Lambda Logic. California Institute of Technology . (Unpublished) http://resolver.caltech.edu/CaltechCSTR:1981.4521tr81

Postscript
See Usage Policy. 2631Kb  

Other (Adobe PDF (2.4MB))
See Usage Policy. 2413Kb 
Use this Persistent URL to link to this item: http://resolver.caltech.edu/CaltechCSTR:1981.4521tr81
Abstract
The main aim of this paper is to formulate "natural" logical foundations for typefree lambdacalculus. The importance of such foundations for analyzing arbitrary order computational properties of programs is emphasized. Lamda logic is a deductive system based on combinatory lambdaterms. Its language is conceived by extending the set of lambdaterms through the addition of new terms which are logical connectives. The model for lamdalogic is Dana Scott's D infinity, which can be represented as a pseudoBoolean 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.4521tr81 
Persistent URL:  http://resolver.caltech.edu/CaltechCSTR:1981.4521tr81 
Usage Policy:  You are granted permission for individual, educational, research and noncommercial reproduction, distribution, display and performance of this work in any format. 
ID Code:  27052 
Collection:  CaltechCSTR 
Deposited By:  Imported from CaltechCSTR 
Deposited On:  02 Jan 2003 
Last Modified:  26 Dec 2012 14:13 
Repository Staff Only: item control page