We present two worked applications of a general framework that can be used to support reasoning about the operational equality relation defined by a programming language semantics. The framework, based on Combinatory Reduction Systems, facilitates the proof of standardization theorems for programming calculi. The importance of standardization theorems to programming language semantics was shown by Plotkin in [Plo75]: standardization together with confluence guarantee that two terms equated in the calculus are semantically equal. We apply the framework to the $\lambda_v$-calculus and to an untyped version of the $\lambda$^{CIL}-calculus. The latter is a basis for an intermediate language used in a compiler.
This paper and the companion paper immediately below were provisionally accepted for publication in a journal. Neither paper was published.
A rewrite system has standardization iff for any rewrite
sequence there is an equivalent one which contracts the redexes in
a standard order. Standardization is extremely useful for finding
normalizing strategies and proving that a rewrite system for a
programming language is sound with respect to the language's
operational semantics.
Although for some rewrite systems the standard-order can be simple,
e.g., left-to-right or outermost first, many systems need a more
delicate order. There are abstract notions of standard order which
always apply, but proofs (often quite difficult) are required that the
rewrite system satisfies a number of axioms and not much guidance is
provided for finding a conrete order that satisfies the abstract
definition.
This paper gives a framework based on combinatory redution systems
(CRS's) which is general enough to handle many programming
languages. If the CRS is orthogonal and fully extended and a good
redex ordering can be found, then a standard order is obtained together
with the standardization theorem. If the CRS also satises further
criteria, then a good redex ordering is mechanially obtained from the
rewrite rules. If the CRS is a construtor system and satises an
additional requirement, then definitions of value and evaluation
providing an operational semantis are automatially obtained together
with a Plotkin/Wadsworth/Felleisen-style standardization theorem.
What follows is a collection of lecture notes for a series of three lectures introducing Scott's domain theory. The lecture notes are not intended to serve as a primary reference but rather as a supplement to a more comprehensive treatment such as [Sch86] or [Sto77].
These notes were presented in a series of guest lectures for Harvard's Spring 1992 section of CS 152 Programming Languages, taught by Stuart Shieber. They were subsequently used in support of courses at other universities.We develop a general framework for deriving abstract domains from concrete semantic domains in the context of first-order recursive schemes and prove several theorems which ensure the correctness (safety) of abstract computations. The abstract domains, which we call Weak Hoare powerdomains, subsume the roles of both the abstract domains and the collecting interpretations in the abstract interpretation literature.
This report was presented at the IFIP Working Group 2.8 on Functional Programming Languages, Paris, France, April 1991. This work was preliminary to Abstract Interpretation in Weak Powerdomains.
We present an efficient algorithm for avoiding unintended name captures during syntax macro transcription in LISP. The algorithm is a hybrid of Kohlbecker's Macro-by-Example and Hygienic algorithms adapted for a representation-independent dialect of LISP. The adaptation yields a substantially different model of syntax macros than is found in S-expression LISP dialects. The most important difference is that the lambda binding patterns become apparent when an abstraction is first (i.e., partially) transcribed in the syntax tree. This allows us to avoid a larger class of name captures than is possible in S-expression dialects such as Scheme where lambda binding patterns are not apparent until the tree is completely transcribed.