CaltechTHESIS
  A Caltech Library Service

Logic from Programming Language Semantics

Citation

Choo, Young-il (1987) Logic from Programming Language Semantics. Dissertation (Ph.D.), California Institute of Technology. doi:10.7907/r9hf-1b88. https://resolver.caltech.edu/CaltechETD:etd-02282008-111427

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, type-free application, infinite structures, self-reference, and reflection) require models that are constructed as limits of partial objects, a logic for dealing with partial objects is required.

Using the D model of the λ-calculus, 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 type-free 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 ordinal-heirarchic construction. A model of objects and multiple inheritance is constructed where objects are self-referential 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:Thesis (Dissertation (Ph.D.))
Subject Keywords:Computer Science
Degree Grantor:California Institute of Technology
Division:Engineering and Applied Science
Major Option:Computer Science
Thesis Availability:Public (worldwide access)
Research Advisor(s):
  • Kajiya, James Thomas
Thesis Committee:
  • Kajiya, James Thomas (chair)
  • Martin, Alain J.
  • Thompson, Frederick B.
  • Kechris, Alexander S.
  • Moschovakis, Yiannis N.
Defense Date:21 May 1987
Record Number:CaltechETD:etd-02282008-111427
Persistent URL:https://resolver.caltech.edu/CaltechETD:etd-02282008-111427
DOI:10.7907/r9hf-1b88
Default Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:811
Collection:CaltechTHESIS
Deposited By: Imported from ETD-db
Deposited On:12 Mar 2008
Last Modified:19 Apr 2021 22:35

Thesis Files

[img]
Preview
PDF (Choo_y_1987.pdf) - Final Version
See Usage Policy.

4MB

Repository Staff Only: item control page