Report Number: CS-TR-89-1288
Institution: Stanford University, Department of Computer Science
Title: Programming and proving with function and control
abstractions
Author: Talcott, Carolyn
Date: October 1989
Abstract: Rum is an intensional semantic theory of function and control
abstractions as computation primitives. It is a mathematical
foundation for understanding and improving current practice
in symbolic (Lisp-style) computation. The theory provides, in
a single context, a variety of semantics ranging from
structures and rules for carrying out computations to an
interpretation as functions on the computation domain.
Properties of powerful programming tools such as functions as
values, streams, aspects of object oriented programming,
escape mechanisms, and coroutines can be represented
naturally. In addition a wide variety of operations on
programs can be treated including program transformations
which introduce function and control abstractions, compiling
morphisms that transform control abstractions into function
abstractions, and operations that transform intensional
properties of programs into extensional properties. The
theory goes beyond a theory of functions computed by
programs, providing tools for treating both intensional and
extensional properties of programs. This provides operations
on programs with meanings to transform as well as meanings to
preserve. Applications of this theory include expressing and
proving properties of particular programs and of classes of
programs and studying mathematical properties of computation
mechanisms. Additional applications are the design and
implementation of interactive computation systems and the
mechanization of reasoning about computation.
These notes are based on lectures given at the Western
Institute of Computer Science summer program, 31 July - 1
August 1986. Here we focus on programming and proving with
function and control abstractions and present a variety of
example programs, properties, and techniques for proving
these properties.
http://i.stanford.edu/pub/cstr/reports/cs/tr/89/1288/CS-TR-89-1288.pdf