Choo, Youngil (1987) Logic from Programming Language Semantics. California Institute of Technology . (Unpublished) http://resolver.caltech.edu/CaltechCSTR:1987.5249tr87

Other (Adobe PDF (2.3MB))
See Usage Policy. 2377Kb 
Use this Persistent URL to link to this item: http://resolver.caltech.edu/CaltechCSTR:1987.5249tr87
Abstract
Logic for reasoning about programs must proceed from the programming language semantics. It is our thesis that programs be considered as mathematical objects that can be reasoned about directly, rather than as linguistic expressions whose meanings are embedded in an intermediate formalism.Since the semantics of many programming language features (including recursion, typefree application, infinite structures, selfreference, and reflection) require models that are constructed as limits of partial objects, a logic for dealing with partial objects is required. Using the D infinity, model of the lambdacalculus, a logic (called continuous logic) for reasoning about partial objects is presented. In continuous logic, the logical operations (negation, implication, and quantification) are defined for each of the finite levels and then extended to the limit, giving us a model of typefree logic. The triples of Hoare Logic are interpreted as partial assertions over the domain of partial states, and contradictions arising from rules for function definitions are analyzed. Recursive procedures and recursive functions are both proved using mathematical induction. A domain of infinite lists is constructed as a model for languages with lazy evaluation and it is compared to an ordinalheirarchic construction. A model of objects and multiple inheritance is constructed where objects are selfreferential states and multiple inheritance is defined using the notion of product of classes. The reflective processor for a language with environment and continuation reflection is constructed as the projective limit of partial reflective processors of finite height.
Item Type:  Report or Paper (Technical Report) 

Group:  Computer Science Technical Reports 
Record Number:  CaltechCSTR:1987.5249tr87 
Persistent URL:  http://resolver.caltech.edu/CaltechCSTR:1987.5249tr87 
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:  26683 
Collection:  CaltechCSTR 
Deposited By:  Imported from CaltechCSTR 
Deposited On:  24 Apr 2001 
Last Modified:  26 Dec 2012 14:02 
Repository Staff Only: item control page