% $Header: /home/bambam/leavens/classes/cs641/general-information/RCS/literature-survey.tex,v 1.4 1994/08/16 21:12:19 leavens Exp leavens $
\documentstyle[11pt]{article}
\input{use-full-page}

\begin{document}
\bibliographystyle{alpha-nolc}
\begin{titlepage}
\vspace*{1.40in}
\begin{center}
{\LARGE Introduction to the Literature} \\
{\LARGE On Semantics} \\
~\\
Gary T. Leavens \\
 ~ \\
TR \#94-15 \\
August 1994
\end{center}

\thispagestyle{empty}
\vfill

\noindent {\bf Keywords:} programming languages,
axiomatic sematics, denotational semantics, operational semantics,
type systems, polymorphism, type theory, data abstraction.


\noindent {\bf 1992 CR Categories:}
D.2.4 [{\em Software Engineering\/}]
	Program Verification;
D.3.1 [{\em Programming Languages\/}]
	Formal Definitions and Theory;
F.3.1 [{\em Logics and Meaning of Programs\/}]
	Specifying and verifying and reasoning about programs;
F.3.2 [{\em Logics and Meaning of Programs\/}]
	Semantics of Programming Languages;
F.3.3 [{\em Logics and Meaning of Programs\/}]
	Studies of Program Constructs.
\vspace{0.5in}

\copyright{} Gary T. Leavens.
Permission is granted for you to make copies for educational and scholarly
purposes, but not for direct commercial advantage, provided this notice
appears on all copies.  All other rights reserved.

\vspace{0.5in}
\begin{center}
Department of Computer Science \\
226 Atanasoff Hall \\
Iowa State University \\
Ames, Iowa 50011-1040, USA
\end{center}
\end{titlepage}

\title{Introduction to the Literature on Semantics}
\author{Gary T. Leavens \\
Department of Computer Science, Iowa State University \\
Ames, IA, 50011-1040 USA \\
leavens@cs.iastate.edu
}
\date{August 16, 1994}  %%%%%%%%%%%%%% change if revise!!! %%%%%%%%%
\maketitle

\begin{abstract}
An introduction to the literature on semantics.
Included are pointers to the literature on
axiomatic semantics, denotational semantics, operational semantics,
and type theory.
\end{abstract}

The following is an selective introduction to the literature on
programming language semantics.
Since this is an {\em introduction},
only a small fraction of the literature can be mentioned here.
References are included because they have intrinsic interest,
although some are included simply because they are the original sources
and are likely to be referenced by others doing related work
(e.g. \cite{Church41}).
If you wish to probe an area more deeply, you might start with the
papers mentioned, follow their references, and also use the
{\em Science Citation Index\/} to see what papers have referenced the
ones mentioned.

\section{General Sources}

Two recent texts that cover many different approaches to semantics are:
\cite{Neilson-Neilson92} \cite{Winskel93}.

Articles discussing principal topics in semantics,
containing many references, appear in volume B of
the {\em Handbook of Theoretical Computer Science\/} \cite{vanLeeuwen90}.

Journals that include a substantial coverage of semantics include
{\em ACM Transactions on Programming Languages and Systems\/} (TOPLAS),
{\em ACM SIGPLAN Notices}, {\em IEEE Transactions on Software Engineering},
{\em Information and Computation\/} (formerly {\em Information and Control},
Academic Press), and {\em Acta Informatica\/} (Springer-Verlag).
Related areas, such as specification and verification have their own journals
(e.g., {\em ACM Transactions on Software Engineering and Methodology},
{\em Science of Computer Programming},
and {\em Formal Aspects of Computing\/}).

Conferences devoted to topics related to semantics include
the IEEE Annual Symposium on Logic in Computer Science (LICS),
the Annual ACM Symposium on Principles of Programming Languages (POPL),
Mathematical Foundations of Programming Semantics (MFPS),
the European Symposium on Programming (ESOP),
the ACM Symposium on LISP and Functional Programming (LFP),
the International Colloquium on Automata, Languages, and Programming (ICALP),
and
the International Symposium on Mathematical Foundations of Computer Science.
Conferences not sponsored by the ACM or IEEE are often available in the
Springer-Verlag series of Lecture Notes in Computer Science (LNCS),
and workshops are often available in the series Workshops in Computing.
The above list does not include conferences devoted to software engineering
(e.g. TAPSOFT)
or particular methods (e.g., category theory)
where some important work is also found.

\section{Mathematical Background}

The basics of universal algebra underly much of the work in semantics.
Gratzer's monumental book \cite{Gratzer79} is a standard reference.
A generalized notion of homomorphism that is often used
in semantics is Statman's logical relations \cite{Statman85},
explained in \cite{Mitchell90b}.

Another foundation is the area of mathematical logic.
A classic approach, using proof theory and model theory is \cite{Enderton72}.
More recent approaches, favoring proof theory (especially predicate logic)
at the expense of model theory and mathematical depth
and emphasizing calculation, include
\cite{Dijkstra-Scholten90} \cite{Gries-Schneider94} \cite{Manna-Waldinger93}.

\subsection{$\lambda$-Calculus}

A standard reference on Church's (untyped) $\lambda$-calculus \cite{Church41}
is Barendregt's book \cite{Barendregt84}.
This book is at times highly technical, but also has sensible definitions
and introductory material.
A shorter account, with a reasonable introduction
to the $\lambda$-calculus is found in \cite{Barendregt90b}.
Other introductions include \cite{Gordon88}
\cite[Sections 6.1--6.2]{Schmidt94}.

The use of $\lambda$-calculus for describing programming languages and as the
inspiration for programming language design has been investigated by Landin
\cite{Landin65} \cite{Landin66} and many others.

For the typed $\lambda$-calculus, a standard reference is
\cite{Girard-Lafont-Taylor89}.
A good introduction can be found in
\cite[Chapter 2]{Gunter92} and \cite[Sections 6.4]{Schmidt94};
both of these texts discuss the semantics of the typed lambda calculus
in detail.
Schmidt's book \cite{Schmidt94}
is also a good introduction to higher-order typed
lambda calculi,
and contains references to work on such higher-order extensions.

\subsection{Category Theory}

Increasingly, especially in denotational semantics,
category theory
\cite{MacLane71} \cite{Lawvere-Schanuel91}
is used in research and for the elegant presentation of results.
For example, categorical logic and the semantics of the typed lambda calculus
are discussed in \cite{Lambek-Scott86}.

For me,
the best introduction seems to be the first 5 chapters of \cite{Goldblatt84}.
There are now several articles \cite{Hoare89}
and books \cite{Barr-Wells90} \cite{Asperti-Longo91} \cite{Pierce91}
\cite{Walters91}
explaining category theory to computer scientists.
For those familiar with (or needing) background
in the semantics of abstract data type specifications,
a good introduction is
Burstall and Goguen's paper \cite{Burstall-Goguen82}.

\section{Axiomatic Semantics}

Hoare pointed out, in his seminal paper \cite[Section 6]{Hoare69},
that one could define a programming language by insisting
``that all implementations of the language shall `satisfy' the axioms
and rules of inference which underlie proofs of the properties of the programs
expressed in the language.''
(However, Hoare attributes this idea to Floyd \cite{Floyd67}.)
Such a semantics is useful because it directly aims to support
program verification.

Because a logic for program verification can be used to define
a programming language, it is difficult to disentangle
work on program verification from work on semantics.
Even if program verification is not itself a form of semantics
(rather, it is an application),
it still provides important motivation for axiomatic semantics.
Therefore, verification is also discussed in this section.

\subsection{Program Verification}

Program verification is concerned with showing that a particular program
meets its specification.
This may be accomplished in several ways;
for example, reasoning from the denotational semantics of the program.
However, the term ``program verification'' is usually implies
a syntactic proof in a specially constructed logic.

Floyd introduced the inductive assertions and well-founded sets methods
for program verification in 1967 \cite{Floyd67}
(see also \cite[Chapter 8]{Loeckx-Sieber87}).
(See \cite{Cousot90} for historical references to the work
of Naur, Von Neumann, and Turing, who anticipated this work.)
The term inductive assertions refers to the assertions that are
put at every branch point in the program's flow graph;
these give rise to verification conditions, which state that
along every path, the correctness of the assertions is preserved.
This shows partial correctness (that the program is correct if it terminates).
The well-founded sets method allows proofs of termination.

Hoare \cite{Hoare69}
was the first to present verification in terms of a logic
for partial correctness that was compositional,
so that program proofs are done by induction on the syntax of programs.
This paper sparked a wealth of research in program verification.
Some surveys of results of this research are \cite{Apt81},
\cite{Fisher-Barringer86}, and \cite{Cousot90},
the latter of which also cites other surveys.
A technical reference is \cite[Chapter 9]{Loeckx-Sieber87}.

A very introductory tutorial on verification
from the software engineering perspective
is \cite[chapter 11]{Liskov-Guttag86}.
The idea of developing a proof of a program at the same time the program is
being developed has been eloquently advocated by Dijkstra and Gries
\cite{Dijkstra76} \cite{Gries81}.
See \cite{Gordon88} for a more theoretical introduction
that treats some aspects of theorem proving.

Concurrency has always been a prime application area,
because concurrent programs are so difficult to debug.
Verification of concurrent programs may be handled with the
Owicki-Gries method \cite{Owicki-Gries76}.
Other techniques use temporal logic (e.g., \cite{Owicki-Lamport82})
and ``transition axioms'' \cite{Lamport89}.
An introduction to Hoare-style verification that discusses concurrent
and distributed programs is \cite{Apt-Olderog91}.

\subsubsection{Abstract Data Types}

Hoare also was the first to consider how verification and abstract data types
interact \cite{Hoare72a}.
His technique allows one to separately verify the correctness of
a type's implementation and programs that use that type,
and is based on the use of representation invariants and abstraction
functions.
A practical implementation of these ideas is found in
\cite{Nakajima-Honda-Nakahara80}.
VDM also uses these techniques \cite{Jones90}.
More recent work in this area is found in \cite{Schoett90}
and \cite{Nipkow89}.

Abstract data types (ADTs) can be specified algebraically
\cite{Guttag-Horowitz-Musser78} \cite{Ehrig-Mahr85}
or by using pre- and post-conditions \cite{Bjorner-Jones82}
\cite{Jones86} \cite{Wing87}.
See \cite[chapter 11]{Liskov-Guttag86}
for a tutorial on program verification using abstract data types.

A related aspect is how the structure of a proof of correctness
may help follow the hierarchical (i.e., layered) structure of
the implementation design \cite{Robinson-Levitt77}
\cite{Guaspari-Marceau-Polak90} \cite{Schoett82}.

\subsubsection{Transformational Programming}

Hoare's original paper \cite{Hoare69},
treated verification as something to be done after a program
was written.
However, Hoare \cite{Hoare71} and others were soon advocating
the development of proofs at the same time as programs.
Dijkstra and Gries became prime advocates of this technique
\cite{Dijkstra76} \cite{Gries81}.
More recent treatments in this style advocate a calculational approach
\cite{Cohen90} \cite{Gries-Schneider94}.
One formalization of this approach is the refinement calculus
\cite{Back-vonWright89a}\cite{Back-vonWright89b}
\cite{Morgan90} 
\cite{Morgan-Gardiner90} \cite{Morgan-Vickers94}.

The idea of formal development of program and proof
has found favor in the functional programming community as well.
The idea behind transformational programming is to transform the
specification of a program into an efficient version
\cite{Burstall-Darlington77}
\cite{Manna-Waldinger80} \cite{Balzer81}
\cite{Cheatham-Holloway-Townley81};
these references are characterized by their work
with equational logic (instead of predicate transformers or a Hoare logic),
their use of algebraic techniques,
and the general focus on functional languages.
Some recent work in this area can be found in \cite{Meertens86}
\cite{Bird89a} \cite{Bird89b} \cite{Talcott88}.
Transformational (or algebraic) techniques also underly the work
on Backus's FP \cite{Backus78}
and Hoare's ``Laws of Programming'' for CSP \cite{Hoare-etal87}.

Contrary to popular belief,
it is also possible to reason ``equationally''
about programs with side-effects and even continuations
\cite{Boehm85} \cite{Felleisen-Friedman86} \cite{Felleisen-Hieb89}.

\subsection{Axiomatic Semantics of Programming Languages}

A classic text on the semantics of programming languages
which treats axiomatic semantics is
\cite{deBakker80}.
Predicte transformer semantics, using the ``weakest precondition'' operator
were advocated by Dijkstra for the definition of his guarded command
language \cite{Dijkstra75}.
A  monograph on predicate transformer semantics
is \cite{Dijkstra-Scholten90}
which goes over notational issues as well
as the underlying mathematics.
A recent monograph that updates \cite{deBakker80} using
predicate transformers is \cite{Hesselink92}.

An example of the use of the axiomatic semantics to describe a programming
language is Hoare and Wirth's axiomatic definition
of Pascal \cite{Hoare-Wirth73}.

The use of an axiomatic semantics as a metric for the ``goodness''
of a language led to two language designs in the 1970s.
Although never implemented fully, Alphard
\cite{Shaw-Wulf-London77} \cite{Shaw81a}
was interesting, and focused on support for both data abstraction
and verification.
The language Euclid \cite{London-etal78} \cite{Popek-etal77}
was implemented, and has been used for various large projects.

\subsection{Algebraic Semantics}

While most axiomatic approaches use Hoare logic or variations
on Hoare logic, there have been a few attempts to use
the techniques of algebra and equational specification
to define programming languages.
Examples include \cite{Manes-Arbib86} \cite{Broy-Wirsing-Pepper87}.

\section{Denotational Semantics}

In contrast to axiomatic semantics,
denotational semantics \cite{Strachey66}
\cite{Scott-Strachey71} \cite{Milne-Strachey76}
\cite{Stoy77} \cite{Scott81} \cite{Schmidt86}
explicitly constructs
mathematical models of programming languages.
A short summary of the denotational approach
can be found in Tennent's article
``The Denotational Semantics of Programming Languages'' \cite{Tennent76}.
A recent survey is found in \cite{Mosses90}.

Introductory texts include \cite{Gordon79}, \cite{Allison86}, \cite{Watt91},
\cite{Schmidt94}.
An excellent new graduate text with more mathematical depth is \cite{Gunter92}.
Standard works on denotational semantics
are the books by Stoy \cite{Stoy77} and Schmidt \cite{Schmidt86},
both of which offer a comprehensive and mathematical treatment.
Schmidt's book \cite{Schmidt86}
has an excellent discussion of domain theory
(see also \cite{Gunter-Scott90})
and can be consulted for references to denotational descriptions of
real languages.

One can use a typed functional programming language, such as Standard ML,
to implement a denotational semantics.
Two descriptions of this idea are \cite{Watt86} \cite{McDonald-Allison89}.

Action semantics, an offshoot of denotational semantics,
is described in \cite{Watt91} and more fully in \cite{Mosses92}.

Schmidt's book \cite{Schmidt86}
also has a discussion of denotational semantics
for concurrent systems.
Hennessy's book has a discussion of more recent work in this area
\cite{Hennessy88a}.
However, denotational approaches to concurrency have not been
as successful as operational semantics.

\section{Operational Semantics}

A compiler or interpreter gives an operational semantics to
a programming language.
This style of semantics dates back to the earliest programming languages,
and was first formalized in the idea of a meta-circular
interpreter for LISP \cite{McCarthy60}.

Meta-circular interpreters are still useful for teaching purposes,
and for prototyping programming language designs.
Several meta-circular interpreters for variants of LISP are discussed in Steele
and Sussman's paper {\em The Art of the Interpreter\/}
\cite{Steele-Sussman78b}.
An excellent and more readily accessible discussion is found in Abelson
and Sussman's book \cite{Abelson-Sussman-Sussman85}, which uses Scheme.
A more detailed treatment of interpreters is found in 
\cite{Kamin90} \cite{Friedman-Wand-Haynes92}.
See \cite{Kiczales-Rivieres-Bobrow91} for an approach using the CLOS
meta-object protocol.

However, for mathematical convenience, one wants something more abstract
than an interpreter or complier.
Landin overcame the circularity problem by the use of an
abstract machine called the ``SECD machine'' \cite{Landin64}
(see also \cite{Henderson80}).

A more systematic style of operational semantics based on rewrite rules
is found in Plotkin's terminal transition systems
\cite{Plotkin77}
also known as ``structural operational semantics''
\cite{Plotkin81} \cite{Hennessy90}
or a ``labeled transition system'' \cite{Astesiano91}.
Hennessy's book is an elementary introduction \cite{Hennessy90}.
This style of semantics has the advantage that it extends naturally
to studies of concurrency \cite{Milner90}.
A classic reference for the operational semantics of concurrent processes
is Milner's book on CCS \cite{Milner80}.
See \cite{Hennessy88a} and \cite{Milner90} for more recent work in this area.

\section{Type Systems}

Much of the modern study of semantics concerns type systems,
which describe many aspects of the static semantics of programming languages.
In contrast, axiomatic, denotational, and operational semantics
describe the dynamic semantics of programming languages.

The purpose of type checking is nicely summarized by Morris
as a mechanism that allows program modules to protect objects
from unwanted discovery, modification, and impersonation \cite{Morris73a}.
Wegbreit's discussion of the extensible language EL1,
is also good background \cite{Wegbreit74}.

Schmidt's recent book \cite{Schmidt94}
starts treats type systems in the context
of programming language semantics.
It also goes deeply into more advanced topics such as
higher-order type systems and predicate-logic typing.

\subsection{Polymorphism}

An introductory survey of modern polymorphic type systems and research results
is Cardelli and Wegner's paper
``On Understanding Types, Data Abstraction and Polymorphism''
\cite{Cardelli-Wegner85}.
See also \cite{Harland84b} \cite{Cardelli91} \cite{Danforth-Tomlinson88};
the latter two have much material related to object-oriented programming.
A still more recent survey is \cite{Mitchell90b}.

Standard references include Girard's system F$\omega$ \cite{Girard71}
(see also \cite{Girard86} \cite{Girard-Lafont-Taylor89}),
and Reynolds independent work \cite{Reynolds74},
sometimes called the Girard-Reynolds second order lambda calculus
(or SOL).
Modern expositions are found in \cite{Mitchell-Plotkin85}
\cite{Mitchell-Harper88} \cite{Reynolds85} \cite{Mitchell90b}
\cite{Cardelli91}.

Other kinds of type information may be incorporated into a type system
and checked at the same time as types \cite{Gifford-Lucassen86}
\cite{Lucassen-Gifford88} \cite{OToole-Gifford89}.

\subsection{Type Theory}

Type theory, narrowly defined, uses the tools of constructive logic
to study polymorphic type systems.
A good introduction can be found in \cite[Chapters 8--10]{Schmidt94}.
Logical inference systems can often be translated directly into type systems
due to the ``Formula as Types'' notion
or the ``Curry-Howard isomorphism'' \cite{Howard80}
\cite[Chapter 3]{Girard-Lafont-Taylor89} \cite{Constable89}.
Thus much research in type theory
lies on the border of mathematics and computer science.
Another motivation is to use type information to capture
behavioral specifications,
thus allowing one to reason about programs in the programming language
\cite{Nordstrom-Peterson83} \cite{Dybjer90}.

The principal groups working on type theory include
deBruijn and others working on AUTOMATH \cite{deBruijn80},
Martin-L\"{o}f's and followers
\cite{Martin-Lof75b} \cite{Martin-Lof82} \cite{Backhouse89},
Constable's group at Cornell has been very active in this area.
Their language PRL which uses constructive mathematics,
is described in the paper ``Proofs as Programs'' \cite{Bates-Constable85}.
A related language is PL/CV3 \cite{Constable-Zlatin84}. 
Coquand and Huet's group is responsible for the
``calculus of constructions'' \cite{Coquand-Huet88}.
A recent survey with more references is \cite{Barendregt-Hemerik90}.

\subsection{Data Abstraction: ADTs and OOP}

Reynolds \cite{Reynolds75} \cite{Reynolds78} (see also \cite{Cook91})
distinguished two ways in which a type system could support data
abstraction.
The first way is to have the language give an object different types
outside and inside a defining module;
this Reynolds called ``user defined types''.
User defined types also go by the name of ``abstract data types'' (ADTs),
and their support in a type system is exemplified by the language CLU
\cite{Liskov-etal77} \cite{Liskov-Guttag86}.

Mitchell and Plotkin connected this approach, ADTs, to the second-order lambda
calculus \cite{Mitchell-Plotkin85}.
This idea has been used to show some representation independence results
\cite{Mitchell86}.
For other work along these lines, see for example,
\cite{MacQueen86} \cite{Cardelli-Leroy90}
\cite{Mitchell90b}.

The second approach to supporting data abstraction Reynolds
called ``procedural data abstraction''.
Today it goes under the more common name of ``object-oriented programming''
(OOP)
\cite{Dahl-Myhraug-Nygaard70} \cite{Birtwistle-etal73}
\cite{Goldberg-Robson83}.
Some languages exemplifying typed support for OOP include
SIMULA \cite{Birtwistle-etal73},
and Eiffel \cite{Meyer88} \cite{Meyer92b},
both of which have insecure type systems \cite{Cook89c}.
The language Trellis/Owl \cite{Schaffert-etal86}
features by-name type checking and subtyping.
By contrast,Emerald \cite{Black-etal86} \cite{Black-etal87}
\cite{Black-Hutchinson90} \cite{Black-Hutchinson91}
and Quest \cite{Cardelli91}
feature structural subtyping.

Some seminal references on types and OOP are reprinted in
\cite{Gunter-Mitchell94}.
Recent theoretical work on types for OOP includes the following
\cite{Cardelli88} \cite{Cardelli88b} \cite{Cardelli-Mitchell89a}
\cite{Amadio-Cardelli90} \cite{Cardelli-etal91} \cite{Cardelli93}
\cite{Canning-etal89a} \cite{Cook-Hill-Canning90} \cite{Cook89c}
\cite{Breazu-Tannen-Gunter-Scedrov90} \cite{Harper-Pierce90}
\cite{Mitchell-Meldal-Madhav91}
\cite{Bruce-etal93} \cite{Bruce-Longo90} \cite{Bruce-Mitchell92} \cite{Abadi93}
\cite{Bruce93}.
(Cardelli is one of the most active in this area,
and most of the literature will cite one of his papers.)
For work that directly bears on multimethods (as in CLOS),
see \cite{Reynolds80}
\cite{Ghelli91a} \cite{Ghelli91b}
\cite{Castagna-Ghelli-Longo92} \cite{Chambers92} \cite{Castagna-Ghelli-Longo93}
\cite{Castagna93} \cite{Chambers-Leavens94}.


\subsection{Type Reconstruction}

Type reconstruction (or type inference) is the process of reconstructing
types for a program that has no type declarations.
A practical and sound algorithm is described in Milner's paper
``A Theory of Type Polymorphism in Programming''
\cite{Milner78}.
Another exposition of this material,
incorporating refinements found in \cite{Damas-Milner82},
is found in \cite{Cardelli87}.

Milner-style type inference system is used in the programming language ML
\cite{Gordon-etal79} \cite{Milner84} \cite{Harper86}
\cite{Harper-MacQueen-Milner86}.
The ideal model has been used to give a semantics to the ML type system
\cite{MacQueen-Plotkin-Sethi86}.

The question of whether one can do type inference for
more powerful type systems has been an active area of research
(e.g., \cite{McCracken84} \cite{Wand89a}).
A recent survey of what is known about such problems is found in
\cite{Tiuryn90}.

See Knight's survey \cite{Knight89}
for a discussion of the central role that unification
plays in type inference and more details on unification itself.

\subsection{Research Languages}

The language Russell was developed at Cornell to investigate how types can be
treated as values.
There are many papers that have appeared about Russell,
but perhaps the best introduction to the language is the paper
``Data Types are Values'' \cite{Donahue-Demers85},
which can be consulted for other references.
Russell has separate mechanisms for building types
and for information hiding;
the same idea is found in Haskell \cite[Pages 387-388]{Hudak89}.
Interesting variations are found in Miranda \cite{Turner85}.

Much recent work has centered around the language ML
and its modern variant Standard ML \cite{Milner84}
\cite{Milner-Tofte-Harper90} \cite{Milner-Tofte91}.
Besides the type inference in its type system mentioned above,
Standard ML has an interesting module system
\cite{MacQueen84} \cite{Harper85b} \cite{Harper-Milner-Tofte87}.

\bibliography{journal-abbrevs,distrib,datatypes,languages,se,old-datatypes,etc}
\end{document}