Mathematical Theory of Computation
Abstract
This project was concerned with the development of correct and reusable software through the use of higher order abstractions (function, control, assignment, process) and reflection. A semantic framework for these notions will be the basis of an experimental system for manipulating and reasoning about programs. The goals of this project were the development of logical formalisms for reasoning about programs that use abstractions and reflection, and the application of these theoretical results to selected software problems. Example applications include (1) clarification of existing programming paradigms, (2) analysis of existing and proposed languages used in the DARPA community for specifying, writing, and transforming programs, and (3) development and implementation of tools for computer aided reasoning about and operating on programs. The accomplishments of this project fit into four categories: (1) logics for reasoning about function and control abstractions; (2) logics for reasoning about data mutation; (3) logics for reasoning about function and control abstractions in the presence of mutable data; and (4) applying methodology for reasoning about programs to the mechanical verification of hardware.
Document Details
- Document Type
- Technical Report
- Publication Date
- Aug 01, 1991
- Accession Number
- ADA239419
Entities
People
- John McCarthy
Organizations
- Stanford University