@comment{SHORT BIBLIOGRAPHY FILE -- JOHN C. REYNOLDS -- February 4, 2012}
@comment{This is an excerpt from reynolds.bib limited to publications
by John C. Reynolds, and books containing such publications}
@comment{This is a master bibliographic file of documents that have been
cited or otherwise used by John Reynolds, who expects to periodically
update the file. Although the file uses the BIBTEX format, there are
a number of additional fields that are not interpreted by standard BIBTEX
styles:
The following fields are interpreted by cmu-bst and cmu-unsrt (which
are bibliographic styles written at Carnegie Mellon):
booksubtitle - The subtitle of a book, part of which is being cited.
dates - The dates of a meeting, as opposed to a date of publication,
which would be given by the month and year fields. If a proceedings
is published the same year as the meeting was held, the year is
omitted from the dates field.
department - The department of the institution, school, or
organization responsible for an technical report, thesis,
or unpublished document.
place - The location of a meeting.
subtitle - The secondary part of a title.
The following fields are not interpreted by either standard or CMU
bibliographic styles:
callno - The library call number (usually for Carnegie Mellon libraries).
checked - The date the entry was checked against the original document
being cited.
comments - Miscellaneous remarks not to be printed.
entered - The date an unchecked entry was placed in the file.
filename - The filename used to obtain the document using ftp.
hidnumber - Same as number (used to avoid printing in certain
bibliographies).
hidseries - Same as series (used to avoid printing in certain
bibliographies).
isbn - The International Standard Book Number.
pfilename - A filename for the document in my nonpublic files.
reprint - Information about one or more places where the cited
document has been reprinted. This information uses the macros
\authorcite and \crosscite to give authors and citation keys.
For example:
reprint = "Reprinted in \authorcite{Gunter and
Mitchell} \crosscite[pages~13--23]{GUNTER94}",
When used with standard Bibtex styles, these macros may be defined
as follows:
\def\authorcite#1{\relax}
\def\crosscite{\cite}
Note that calls of \cite from within bibliographic entries may
require repeated runs of BIBTEX in alternation with LATEX.
updated - The date an entry was last altered (if this date is after
November 8, 1990 and also after the date in the checked or
entered field).
url - Address of a web page. (Spaces have been inserted in some of
these entries to produce line breaks in certain bibliographies.)
It should also be noted that the month field often contains a more specific
date than just the name of a month. When this entry would conclude with an
integer (day of the month), a comma is appended.
Abbreviations for months and journal names are not used.
}
@book{GRIES78,
editor = "David Gries",
title = "Programming Methodology",
subtitle = "A Collection of Articles by Members of IFIP WG 2.3",
publisher = "Springer-Verlag",
address = "New York",
year = "1978",
pages = "xiv+440",
checked = "12 May 1997"}
@book{GUNTER94,
author = "Gunter, Carl A. and Mitchell, John C.",
title = "Theoretical Aspects of Object-Oriented Programming",
subtitle = "Types, Semantics, and Language Design",
publisher = "MIT Press",
address = "Cambridge, Massachusetts",
year = "1994",
pages = "vii+548",
isbn = "0-262-07155-X",
checked = "6 December 1994"}
@book{OHEARN97,
editor = "O'Hearn, Peter W. and Tennent, Robert D.",
title = "{ALGOL}-like Languages",
publisher = "Birkh{\"a}user",
address = "Boston, Massachusetts",
year = "1997",
note = "Two volumes",
pages = "viii+288",
isbn = "0-8176-3936-5 (set) 0-8176-3880-6 (vol.~1) 0-8176-3937-3 (vol.~2)",
checked = "9 May 1997",
updated = "14 July 1997"}
@article{OHEARN97B,
author = "O'Hearn, Peter W. and Reynolds, John C.",
title = "From Algol to Polymorphic Linear Lambda-Calculus",
journal = "Journal of the ACM",
volume = "47",
number = "1",
month = "January",
year = "2000",
pages = "167--223",
filename = "algoltopolylin",
abstract = "In a linear-typed functional language one can define functions
that consume their arguments in the process of computing their results.
This is reminiscent of state transformations in imperative languages, where
execution of an assignment statement alters the contents of the store. We
explore this connection by translating two variations on Algol 60 into a
purely functional language with polymorphic linear types. On the one hand,
the translations lead to a semantic analysis of Algol-like programs, in terms
of a model of the linear language. On the other hand, they demonstrate that
a linearly-typed functional language can be at least as expressive as Algol.",
checked = "20 April 2000"}
@inproceedings{OHEARN01,
author = "O'Hearn, Peter W. and Reynolds, John C. and Yang, Hongseok",
title = "Local Reasoning about Programs that Alter Data Structures",
booktitle = "Computer Science Logic",
booksubtitle = "15th International Workshop, CSL 2001, 10th Annual Conference of the EACSL, Proceedings",
editor = "Laurent Fribourg",
date = "September 10--13",
place = "Paris",
series = "Lecture Notes in Computer Science",
volume = "2142",
publisher = "Springer-Verlag",
address = "Berlin",
year = "2001",
pages = "1--19",
filename = "localreasoning",
comments = "slides in ohearn/localreasonsl01-02.ps",
abstract = "We describe an extension of Hoare's logic for reasoning about
programs that alter data structures. We consider a low-level storage
model based on a heap with associated lookup, update, allocation and
deallocation operations, and unrestricted address arithmetic. The assertion
language is based on a possible worlds model of the logic of bunched
implications, and includes spatial conjunction and implication connectives
alongside those of classical logic. Heap operations are axiomatized
using what we call the `small axioms', each of which mentions only those
cells accessed by a particular command. Through these and a number of
examples we show that the formalism supports local reasoning: A specification
and proof can concentrate on only those cells in memory that a program
accesses.
This paper builds on earlier work by Burstall, Reynolds, Ishtiaq, and O'Hearn
on reasoning about data structures.",
entered = "12 June 2001",
updated = "14 January 2002"}
@inproceedings{OHEARN04,
author = "O'Hearn, Peter W. and Yang, Hongseok and Reynolds, John C.",
title = "Separation and Information Hiding",
booktitle = "Conference Record of POPL 2004: The 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages",
publisher = "ACM Press",
address = "New York",
dates = "January 14--16",
year = "2004",
place = "Venice, Italy",
pages = "268--280",
comments = "Superceded by OHEARN09",
filename = "sephide",
abstract = "We investigate proof rules for information hiding, using the
recent formalism of separation logic. In essence, we use the separating
conjunction to partition the internal resources of a module from those
accessed by the module's clients. The use of a logical connective gives
rise to a form of dynamic partitioning, where we track the transfer of
ownership of portions of heap storage between program components. It
also enables us to enforce separation in the presence of mutable data
structures with embedded addresses that may be aliased.",
checked = "31 January 2004"}
@article{OHEARN09,
author = "O'Hearn, Peter W. and Yang, Hongseok and Reynolds, John C.",
title = "Separation and Information Hiding",
journal = "ACM Transactions on Programming Languages and Systems",
volume = "31",
number = "3",
month = "April",
year = "2009",
pages = "11:1--50",
comments = "supercedes OHEARN04",
abstract = "We investigate proof rules for information hiding, using the
formalism of separation logic. In essence, we use the separating
conjunction to partition the internal resources of a module from those
accessed by the module's clients. The use of a logical connective gives
rise to a form of dynamic partitioning, where we track the transfer of
ownership of portions of heap storage between program components. It
also enables us to enforce separation in the presence of mutable data
structures with embedded addresses that may be aliased.",
checked = "5 February 2010"}
@inproceedings{REDDY12,
author = "Uday S. Reddy and John C. Reynolds",
title = "Syntactic Control of Interference for Separation Logic",
booktitle = "POPL 2012: Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages",
publisher = "ACM",
address = "New York",
dates = "January 25-27",
year = "2012",
place = "Philadelphia",
pages = "323--336",
filename = "sciseplog",
abstract = "Separation Logic has witnessed tremendous success in recent years
in reasoning about programs that deal with heap storage. Its success owes to
the fundamental principle that one should keep separate areas of the heap
storage separate in program reasoning. However, the way Separation Logic deals
with program variables continues to be based on traditional Hoare Logic without
taking any benefit of the separation principle. This has led to unwieldy proof
rules suffering from lack of clarity as well as questions surrounding their
soundness. In this paper, we extend the separation idea to the treatment of
variables in Separation Logic, especially Concurrent Separation Logic, using
the system of Syntactic Control of Interference proposed by Reynolds in 1978.
We extend the original system with permission algebras, making it more
powerful and able to deal with the issues of concurrent programs. The result
is a streamlined presentation of Concurrent Separation Logic, whose rules are
memorable and soundness obvious. We also include a discussion of how the new
rules impact the semantics and devise static analysis techniques to infer the
required permissions automatically.",
entered = "3 February 2012"}
@inproceedings{REYNOLDS65,
author = "Reynolds, John C.",
title = "An Introduction to the {COGENT} Programming System",
booktitle = "Association for Computing Machinery Proceedings of the 20th National Conference",
publisher = "Lewis Winner",
address = "New York",
dates = "August 24--26",
place = "Cleveland, Ohio",
year = "1965",
pages = "422--436",
filename = "cogent",
abstract = "The COGENT programming system is a compiler whose input language
is designed to describe symbolic or linguistic manipulation algorithms. It
represents an attempt to unify the concepts of syntax-directed compilation and
recursive list-processing. Basically a COGENT program is a list-processing
program in which the list structures normally represent phrases of one or
more object languages. Correspondingly, the COGENT language itself contains
two major constructions: productions, which define the object language
syntax, and generator definitions, which define list-processing subroutines.",
checked = "22 August 1990",
updated = "9 May 2001"}
@inproceedings{REYNOLDS69A,
author = "Reynolds, John C.",
title = "A Generalized Resolution Principle Based Upon Context-Free Grammars",
booktitle = "Information Processing 68",
booksubtitle = "Proceedings of IFIP Congress 1968",
dates = "August 5--10, 1968",
place = "Edinburgh",
editor = "A. J. H. Morrell",
volume = "2",
publisher = "North-Holland",
address = "Amsterdam",
year = "1969",
pages = "1405--1411",
callno = "004 I613i 1968",
checked = "23 August 1990"}
@inproceedings{REYNOLDS69B,
author = "Reynolds, John C.",
title = "Automatic Computation of Data Set Definitions",
booktitle = "Information Processing 68",
booksubtitle = "Proceedings of IFIP Congress 1968",
dates = "August 5--10, 1968",
place = "Edinburgh",
editor = "A. J. H. Morrell",
volume = "1",
publisher = "North-Holland",
address = "Amsterdam",
year = "1969",
pages = "456--461",
callno = "004 I613i 1968",
filename = "autodataset",
abstract = "Most programming systems which attempt to provide flexible and
efficient data representations require the user to specify the range of
variables, parameters, and functions by extensive and detailed data structure
declarations. The purpose of this paper is to suggest that much of this
declarative information is redundant, and can be inferred from the
non-declarative portion of the program,, Specifically, in the context of a
restricted but non-trivial programming language, pure LISP, a method is
given for constructing a data set description of the results of a function
from a program for the function and a data set description of its arguments",
checked = "23 August 1990",
updated = "9 May 2001"}
@incollection{REYNOLDS69C,
author = "Reynolds, John C.",
title = "Transformational Systems and the Algebraic Structure of Atomic Formulas",
booktitle = "Machine Intelligence 5",
editor = "Bernard Meltzer and Donald Michie",
publisher = "Edinburgh University Press",
address = "Edinburgh, Scotland",
year = "1969",
comments = "Some copies are copyrighted 1970",
pages = "135--151",
filename = "transysalg",
abstract = "If the set of atomic formulas is augmented by adding a `universal
formula' and a `null formula', then the equivalence classes of this set under
alphabetic variation form a complete non-modular lattice, with `instance'
as the partial ordering, `greatest common instance' as the meet operation,
and `least common generalization' as the join operation. The greatest common
instance of two formulas can be obtained from Robinson's Unification Algorithm.
An algorithm is given for computing the least common generalization of two
formulas, the covering relation of the lattice is determined, bounds are
obtained on the length of chains from one formula to another, and it is shown
that any formula is the least common generalization of its set of ground
instances.
A transformational system is a finite set of clauses containing only units
and transformations, which are clauses containing exactly one positive and one
negative literal. It is shown that every unsatisfiable transformational system
has a refutation where every resolution has at least one resolvend which is an
initial clause. An algorithm is given for computing a common generalization of
all atomic formulas which can be derived from a transformational system, and
it is shown that there is no decision procedure for transformational systems.",
checked = "22 August 1990",
updated = "9 May 2001"}
@techreport{REYNOLDS69D,
author = "Reynolds, John C.",
title = "{GEDANKEN} -- {A} Simple Typeless Language Which Permits Functional Data Structures and Coroutines",
type = "Report",
number = "ANL--7621",
institution = "Argonne National Laboratory",
department = "Applied Mathematics Division",
month = "September",
address = "Argonne, Illinois",
year = "1969",
checked = "24 August 1990"}
@unpublished{REYNOLDS69E,
author = "Reynolds, John C.",
title = "A Set-Theoretic Approach to the Concept of Type",
institution = "Argonne National Laboratory",
address = "Argonne, Illinois",
note = "Unpublished working material for the NATO Science Committee Conference on Techniques in Software Engineering, Rome, Italy, October 29--31",
year = "1969",
checked = "24 August 1990",
updated = "8 May 1997"}
@article{REYNOLDS70,
author = "Reynolds, John C.",
title = "{GEDANKEN} -- A Simple Typeless Language Based on the Principle of Completeness and the Reference Concept",
journal = "Communications of the ACM",
month = "May",
volume = "13",
number = "5",
year = "1970",
pages = "308--319",
filename = "gedanken",
abstract = "GEDANKEN is an experimental programming language with the following
characteristics. (1) Any value which is permitted in some context of the
language is permissible in any other meaningful context. In particular,
functions and labels are permissible results of functions and values of
variables. (2) Assignment and indirect addressing are formalized by
introducing values, called references, which in turn possess other values.
The assignment operation always affects the relation between some reference
and its value. (3) All compound data structures are treated as functions.
(4) Type declarations are not permitted.
The functional approach to data structures and the use of references insure
that any process which accepts some data structure will accept any logically
equivalent structure, regardless of its internal representation. More
generally, any data structure may be implicit; i.e.~it may be specified by
giving an arbitrary algorithm for computing or accessing its components.
The existence of label variables permits the construction of co-routines,
quasi-parallel processes, and other unorthodox control mechanisms.
A variety of programming examples illustrates the generality of the language.
Limitations and possible extensions are discussed briefly.",
checked = "4 September 1990",
updated = "9 May 2001"}
@inproceedings{REYNOLDS72A,
author = "Reynolds, John C.",
title = "Definitional Interpreters for Higher-Order Programming Languages",
booktitle = "Proceedings of the ACM Annual Conference",
volume = "2",
publisher = "ACM",
address = "New York",
dates = "August",
year = "1972",
place = "Boston, Massachusetts",
pages = "717--740",
reprint = "Reprinted as \authorcite{Reynolds} \crosscite{REYNOLDS98D}",
filename = "defint",
abstract = "Higher-order programming languages (i.e., languages in which procedures
or labels can occur as values) are usually defined by interpreters that are
themselves written in a programming language based on the lambda calculus (i.e., an
applicative language such as pure LISP). Examples include McCarthy's definition
of LISP, Landin's SECD machine, the Vienna definition of PL/I, Reynolds'
definitions of GEDANKEN, and recent unpublished work by L. Morris and
C. Wadsworth. Such definitions can be classified according to whether the
interpreter contains higher-order functions, and whether the order of
application (i.e., call by value versus call by name) in the defined language
depends upon the order of application in the defining language. As an example,
we consider the definition of a simple applicative programming language by
means of an interpreter written in a similar language. Definitions in each
of the above classifications are derived from one another by informal but
constructive methods. The treatment of imperative features such as jumps and
assignment is also discussed.",
checked = "22 May 1990",
updated = "8 September 1998"}
@techreport{REYNOLDS72B,
author = "Reynolds, John C.",
title = "Notes on a Lattice-Theoretic Approach to the Theory of Computation",
institution = "Syracuse University",
department = "School of Computer and Information Science",
address = "Syracuse, New York",
month = "October",
year = "1972",
type = "Report",
note = "Revised March 1979",
pages = "iv+160",
checked = "17 August 1990"}
@inproceedings{REYNOLDS74A,
author = "Reynolds, John C.",
title = "On the Relation between Direct and Continuation Semantics",
booktitle = "Automata, Languages and Programming",
booksubtitle = "2nd Colloquium",
dates = "July 29--August 2",
place = "Saarbr{\"u}cken",
editor = "Jacques Loeckx",
series = "Lecture Notes in Computer Science",
volume = "14",
publisher = "Springer-Verlag",
address = "Berlin",
year = "1974",
pages = "141--156",
filename = "reldircont",
abstract = "The use of continuations in the definition of programming
languages has gained considerable currency recently, particularly in
conjunction with the lattice-theoretic methods of D.~Scott. Although
continuations are apparently needed to provide a mathematical semantics for
non-applicative control features, they are unnecessary for the definition of
a purely applicative language, even when call-by-value occurs. This raises
the question of the relationship between the direct and the continuation
semantic functions for a purely applicative language. We give two theorems
which specify this relationship and show that, in a precise sense, direct
semantics are included in continuation semantics.
The heart of the problem is the construction of a relation which must be a
fixed-point of a non-monotonic `relational functor.' A general method is
given for the construction of such relations between recursively defined
domains.",
checked = "18 July 1989",
updated = "9 May 2001"}
@incollection{REYNOLDS74B,
author = "Reynolds, John C.",
title = "Relational and Continuation Semantics for a Simple Imperative Language",
booktitle = "Th{\'e}orie des Algorithmes, des Langages et de la Programmation",
series = "S{\'e}minaires IRIA",
editor = "Maurice Nivat",
publisher = "IRIA (INRIA)",
address = "Rocquencourt, France",
year = "1974",
pages = "51--58",
checked = "22 August 1990",
updated = "6 May 1997"}
@inproceedings{REYNOLDS74C,
author = "Reynolds, John C.",
title = "Towards a Theory of Type Structure",
booktitle = "Programming Symposium",
booksubtitle = "Proceedings, Colloque sur la Programmation",
dates = "April 9--11",
place = "Paris, France",
editor = "B. Robinet",
series = "Lecture Notes in Computer Science",
volume = "19",
publisher = "Springer-Verlag",
address = "Berlin",
year = "1974",
pages = "408--425",
filename = "theotypestr",
abstract = "The type structure of programming languages has been the subject
of an active development characterized by continued controversy over basic
principles. In this paper, we formalize a view of these principles somewhat
similar to that of J. H. Morris. We introduce an extension of the typed
lambda calculus which permits user-defined types and polymorphic functions,
and show that the semantics of this language satisfies a representation
theorem which embodies our notion of a `correct' type structure.",
checked = "22 August 1990",
updated = "9 May 2001"}
@inproceedings{REYNOLDS75A,
author = "Reynolds, John C.",
title = "On the Interpretation of {S}cott's Domains",
booktitle = "Informatica Teorica",
place = "Rome, Italy",
dates = "Febraury 6--9, 1973",
series = "Symposia Mathematica",
volume = "15",
year = "1975",
publisher = "Instituto Nazionale di Alta Matematica Roma",
note = "Distributed by Academic Press, London",
pages = "123--135",
filename = "intdomain",
abstract = "The lattice-theoretic approach to the theory of computation,
developed by D.~Scott, is based on assumptions that the data spaces
manipulated by a computation are complete lattices whose partial ordering
represents a notion of approximation, and that the computable functions
between such data spaces are continuous (in an appropriate sense). Since these
assumptions lead to conclusions which are quite different from the conventional
theory of computation, it is important to understand their interpretation in
terms of actual computational processes.
We consider non-terminating computational processes whose input and output are
enumerations of sets of messages. Given a relationship of satisfaction between
the universe of messages and some universe of models, we define the meaning of
a message set to be the set of those models which satisfy all of its members,
and we define the domain to be the range of this meaning function. In this
interpretation, Scott's axioms can be justified by physical limitations of the
communication between the computational processes and their environments.",
checked = "23 August 1990",
upated = "9 May 2001"}
@inproceedings{REYNOLDS75B,
author = "Reynolds, John C.",
title = "User-Defined Types and Procedural Data Structures as Complementary Approaches to Data Abstraction",
booktitle = "New Directions in Algorithmic Languages 1975",
dates = "August 25--29",
place = "Munich",
editor = "Stephen A. Schuman",
organization = "IFIP Working Group 2.1 on {A}lgol",
publisher = "INRIA",
address = "Rocquencourt, France",
year = "1975",
pages = "157--168",
comment = "same as REYNOLDS78B",
reprint = "Reprinted in \authorcite{Gries} \crosscite[pages~309--317]{GRIES78}, and \authorcite{Gunter and Mitchell} \crosscite[pages~13--23]{GUNTER94}",
filename = "compdataabstr",
abstract = "User-defined types (or modes) and procedural (or functional) data
structures are complementary methods for data abstraction, each providing a
capability lacked by the other. With user-defined types, all information about
the representation of a particular kind of data is centralized in a type
definition and hidden from the rest of the program. With procedural data
structures, each part of the program which creates data can specify its own
representation, independently of any representations used elsewhere for the
same kind of data. However, this decentralization of the description of
data is achieved at the cost of prohibiting primitive operations from
accessing the representations of more than one data item. The contrast
between these approaches is illustrated by a simple example.",
checked = "24 May 1989",
updated = "9 May 2001"}
@article{REYNOLDS77,
author = "Reynolds, John C.",
title = "Semantics of the Domain of Flow Diagrams",
journal = "Journal of the ACM",
month = "July",
volume = "24",
number = "3",
year = "1977",
pages = "484--503",
filename = "domflowdiag",
abstract = "A domain of flow diagrams similar to that proposed by Scott, a
domain of linear flow diagrams proposed by Goguen et al., a domain of decision
table diagrams involving infinitary branching, and a domain of processes based
on the ideas of Milner and Bekic are each provided with a direct semantics
closely related to partial-function semantics, and a continuation semantics
similar to that developed by Morris and Wadsworth. It is shown that there
is a variety of meaning-preserving continuous functions among these
language-like domains, that every direct semantics possesses an
`equivalent' continuation semantics, and that there is a particular
continuation semantics which always gives distinct meanings to distinct
processes. The proofs utilize the algebraic methods of Goguen et al., which
are extended to continuous algebras with operations whose arguments can be
indexed by infinite sets or even domains.",
checked = "18 June 1990",
updated = "9 May 2001"}
@inproceedings{REYNOLDS78A,
author = "Reynolds, John C.",
title = "Syntactic Control of Interference",
booktitle = "Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages",
publisher = "ACM",
address = "New York",
place = "Tucson, Arizona",
dates = "January 23--25",
year = "1978",
pages = "39--46",
reprint = "Reprinted in \authorcite{O'Hearn and Tennent} \crosscite[vol.~1, pages~273--286]{OHEARN97}",
filename = "syncontrol",
abstract = "In programming languages which permit both assignment and procedures,
distinct identifiers can represent data structures which share storage or
procedures with interfering side effects. In addition to being a direct
source of programming errors, this phenomenon, which we call interference,
can impact type structure and parallelism. We show how to eliminate these
difficulties by imposing syntactic restrictions, without prohibiting the
kind of constructive interference which occurs with higher-order procedures
or Simula classes. The basic idea is to prohibit interference between
identifiers, but to permit interference among components of collections
named by single identifiers.",
checked = "17 June 1988",
updated = "10 May 1997"}
@incollection{REYNOLDS78B,
author = "Reynolds, John C.",
title = "User-Defined Types and Procedural Data Structures as Complementary Approaches to Data Abstraction",
booktitle = "Programming Methodology",
booksubtitle = "A Collection of Articles by Members of IFIP WG 2.3",
editor = "David Gries",
publisher = "Springer-Verlag",
address = "New York",
year = "1978",
pages = "309--317",
reprint = "Reprinted in \authorcite{Gunter and Mitchell} \crosscite[pages~13--23]{GUNTER94}",
comments = "In GRIES78, same as REYNOLDS75B",
filename = "compdataabstr",
abstract = "User-defined types (or modes) and procedural (or functional) data
structures are complementary methods for data abstraction, each providing a
capability lacked by the other. With user-defined types, all information about
the representation of a particular kind of data is centralized in a type
definition and hidden from the rest of the program. With procedural data
structures, each part of the program which creates data can specify its own
representation, independently of any representations used elsewhere for the
same kind of data. However, this decentralization of the description of
data is achieved at the cost of prohibiting primitive operations from
accessing the representations of more than one data item. The contrast
between these approaches is illustrated by a simple example.",
checked = "22 August 1990",
updated = "9 May 2001"}
@incollection{REYNOLDS78C,
author = "Reynolds, John C.",
title = "Programming with Transition Diagrams",
booktitle = "Programming Methodology",
booksubtitle = "A Collection of Articles by Members of IFIP WG 2.3",
editor = "David Gries",
publisher = "Springer-Verlag",
address = "New York",
year = "1978",
pages = "153--165",
comments = "in GRIES78",
filename = "progtransdiag",
abstract = "In situations where the avoidance of goto statements would be
inhibiting, programs can be methodically constructed by using transition
diagrams. The key requirement is that the relevant assertions must be simple
enough to permit exhaustive reasoning. The method is illustrated by programs
for fast exponentiation, merging, and path-finding in a directed graph.",
checked = "22 August 1990",
updated = "9 May 2001"}
@article{REYNOLDS79,
author = "Reynolds, John C.",
title = "Reasoning About Arrays",
journal = "Communications of the ACM",
month = "May",
volume = "22",
number = "5",
year = "1979",
pages = "290--299",
filename = "arrayreason",
abstract = "A variety of concepts, laws, and notations are presented which
facilitate reasoning about arrays. The basic concepts include intervals and
their partitions, functional restriction, images, pointwise extension of
relations, ordering, single-point variation of functions, various equivalence
relations for array values, and concatenation. The effectiveness of these
ideas is illustrated by informal descriptions of algorithms for binary search
and merging, and by a short formal proof.",
checked = "4 September 1990",
updated = "9 May 2001"}
@inproceedings{REYNOLDS80,
author = "Reynolds, John C.",
title = "Using Category Theory to Design Implicit Conversions and Generic Operators",
booktitle = "Semantics-Directed Compiler Generation",
booksubtitle = "Proceedings of a Workshop",
place = "Aarhus, Denmark",
dates = "January 14--18",
editor = "Neil D. Jones",
series = "Lecture Notes in Computer Science",
volume = "94",
publisher = "Springer-Verlag",
address = "Berlin",
year = "1980",
pages = "211--258",
reprint = "Reprinted in \authorcite{Gunter and Mitchell} \crosscite[pages~25--64]{GUNTER94}",
filename = "cattheodesign",
abstract = "A generalization of many-sorted algebras, called category-sorted
algebras, is defined and applied to the language-design problem of avoiding
anomalies in the interaction of implicit conversions and generic operators.
The definition of a simple imperative language (without any binding mechanisms)
is used as an example.",
checked = "22 August 1990",
updated = "9 May 2001"}
@inproceedings{REYNOLDS81A,
author = "Reynolds, John C.",
title = "The Essence of {A}lgol",
booktitle = "Algorithmic Languages",
booksubtitle = "Proceedings of the International Symposium on Algorithmic Languages",
place = "Amsterdam",
dates = "October 26--29",
editor = "Jaco W. de Bakker and J. C. van Vliet",
publisher = "North-Holland",
address = "Amsterdam",
year = "1981",
pages = "345--372",
filename = "essence",
reprint = "Reprinted in \authorcite{O'Hearn and Tennent} \crosscite[vol.~1, pages~67--88]{OHEARN97}",
abstract = "Although Algol 60 has been uniquely influential in programming language
design, its descendants have been significantly different than their prototype.
In this paper, we enumerate the principles that we believe embody the essence of
Algol, describe a model that satisfies these principles, and illustrate this model
with a language that, while more uniform and general, retains the character of Algol.",
checked = "17 June 1988",
updated = "10 May 1997"}
@book{REYNOLDS81B,
author = "Reynolds, John C.",
title = "The Craft of Programming",
publisher = "Prentice-Hall International",
address = "London",
year = "1981",
pages = "xiii+434",
isbn = "0-13-188862-5",
callno = "510.784 R46c or QA76.6.R46",
filename = "craftprog",
checked = "17 June 1988",
updated = "4 April 2002"}
@techreport{REYNOLDS81C,
author = "Reynolds, John C.",
title = "Idealized {A}lgol and its Specification Logic",
type = "Report",
number = "1--81",
institution = "Syracuse University",
department = "School of Computer and Information Science",
address = "Syracuse, New York",
month = "July",
year = "1981",
reprint = "Reprinted as \authorcite{Reynolds} \crosscite{REYNOLDS82} and in \authorcite{O'Hearn and Tennent} \crosscite[vol.~1, pages~125--156]{OHEARN97}",
filename = "speclogic",
abstract = "Specification logic is a new formal system for program proving
that is applicable to programming languages, such as Algol, whose procedure
mechanism can be described by the copy rule. The starting point of its
development is the recognition that, in the presence of an Algol-like
procedure mechanism, {\em specifications}, such as Hoare's $\{P\}\;S\;\{Q\}$
must be regarded as predicates about environments (in the sense of Landin).
The logic provides additional kinds of specifications describing
interference between variables and other entities, and methods for compounding
specifications by using implication, conjunction, and universal quantification.
The result is a system in which one can infer {\em universal} specifications
that hold in all environments.",
checked = "24 August 1990",
updated = "10 May 1997"}
@inproceedings{REYNOLDS82,
author = "Reynolds, John C.",
title = "Idealized {A}lgol and its Specification Logic",
booktitle = "Tools and Notions for Program Construction",
booksubtitle = "An advanced course",
dates = "December 7--18, 1981",
place = "Nice, France",
editor = "Danielle N{\'e}el",
publisher = "Cambridge University Press",
address = "Cambridge, England",
year = "1982",
pages = "121--161",
comments = "Same as REYNOLDS81C",
reprint = "Reprinted in \authorcite{O'Hearn and Tennent} \crosscite[vol.~1, pages~125--156]{OHEARN97}",
filename = "speclogic",
abstract = "Specification logic is a new formal system for program proving
that is applicable to programming languages, such as Algol, whose procedure
mechanism can be described by the copy rule. The starting point of its
development is the recognition that, in the presence of an Algol-like
procedure mechanism, {\em specifications}, such as Hoare's $\{P\}\;S\;\{Q\}$
must be regarded as predicates about environments (in the sense of Landin).
The logic provides additional kinds of specifications describing
interference between variables and other entities, and methods for compounding
specifications by using implication, conjunction, and universal quantification.
The result is a system in which one can infer {\em universal} specifications
that hold in all environments.",
checked = "24 May 1989",
updated = "10 May 1997"}
@inproceedings{REYNOLDS83,
author = "Reynolds, John C.",
title = "Types, Abstraction and Parametric Polymorphism",
booktitle = "Information Processing 83",
booksubtitle = "Proceedings of the IFIP 9th World Computer Congress",
place = "Paris, France",
dates = "September 19--23, 1983",
editor = "R. E. A. Mason",
publisher = "Elsevier Science Publishers B. V. (North-Holland)",
address = "Amsterdam",
year = "1983",
pages = "513--523",
callno = "004 I613ia 1983",
filename = "typesabpara",
abstract = "We explore the thesis that type structure is a syntactic discipline
for maintaining levels of abstraction. Traditionally, this view has been
formalized algebraically, but the algebraic approach fails to encompass
higher-order functions. For this purpose, it is necessary to generalize
homomorphic functions to relations; the result is an `abstraction' theorem
that is applicable to the typed lambda calculus and various extensions,
including user-defined types. Finally, we consider polymorphic functions,
and show that the abstraction theorem captures Strachey's concept of
parametric, as opposed to ad hoc, polymorphism.",
checked = "January 1988",
updated = "9 May 2001"}
@inproceedings{REYNOLDS83A,
author = "Reynolds, John C.",
title = "An Introduction to Specification Logic (Abstract of Invited Lecture)",
booktitle = "Logic of Programs",
booksubtitle = "Proceedings 1983",
place = "Pittsburgh",
dates = "June 6--8",
editor = "Edmund Clarke and Dexter Kozen",
series = "Lecture Notes in Computer Science",
volume = "164",
publisher = "Springer-Verlag",
address = "Berlin",
year = "1984",
pages = "442",
checked = "11 February 2002"}
@inproceedings{REYNOLDS84,
author = "Reynolds, John C.",
title = "Polymorphism is not Set-Theoretic",
booktitle = "Semantics of Data Types",
booksubtitle = "International Symposium",
place = "Sophia-Antipolis, France",
dates = "June 27--29",
editor = "Gilles Kahn and David B. MacQueen and Gordon D. Plotkin",
series = "Lecture Notes in Computer Science",
volume = "173",
publisher = "Springer-Verlag",
address = "Berlin",
year = "1984",
pages = "145--156",
checked = "January 1988"}
@inproceedings{REYNOLDS85,
author = "Reynolds, John C.",
title = "Three Approaches to Type Structure",
booktitle = "Mathematical Foundations of Software Development",
booksubtitle = "Proceedings of the International Joint Conference on Theory and Practice of Software Development (TAPSOFT), Volume 1: Colloquium on Trees in Algebra and Programming (CAAP'85)",
place = "Berlin",
dates = "March 25--29",
editor = "Hartmut Ehrig and Christiane Floyd and Maurice Nivat and James W. Thatcher",
series = "Lecture Notes in Computer Science",
volume = "185",
publisher = "Springer-Verlag",
address = "Berlin",
year = "1985",
pages = "97--138",
checked = "21 August 1990",
updated = "27 May 1998"}
@inproceedings{REYNOLDS87,
author = "Reynolds, John C.",
title = "Conjunctive Types and {A}lgol-like Languages (Abstract of Invited Lecture)",
booktitle = "Proceedings Symposium on Logic in Computer Science",
publisher = "IEEE Computer Society Press",
address = "Washington, D.C.",
dates = "June 22--25",
year = "1987",
place = "Ithaca, New York",
pages = "119",
callno = "004598p 1987 2nd",
checked = "15 October 1990",
updated = "13 August 1982"}
@techreport{REYNOLDS88,
author = "Reynolds, John C. and Plotkin, Gordon D.",
title = "On Functors Expressible in the Polymorphic Typed Lambda Calculus",
note = "A preliminary version of a paper to appear in Information and Computation",
type = "Report",
number = "CMU--CS--88--125",
institution = "Carnegie Mellon University",
department = "Computer Science Department",
address = "Pittsburgh, Pennsylvania",
month = "March 16,",
year = "1988",
comments = "same as REYNOLDS90 and superseded by REYNOLDS90B and REYNOLDS93B",
checked = "24 May 1988",
updated = "29 July 1993"}
@techreport{REYNOLDS88B,
author = "Reynolds, John C.",
title = "Preliminary Design of the Programming Language {F}orsythe",
type = "Report",
number = "CMU--CS--88--159",
institution = "Carnegie Mellon University",
department = "Computer Science Department",
address = "Pittsburgh, Pennsylvania",
month = "June 21,",
year = "1988",
comments = "superseded by REYNOLDS96",
checked = "7 April 1989",
updated = "13 June 1996"}
@inproceedings{REYNOLDS89,
author = "Reynolds, John C.",
title = "Syntactic Control of Interference, Part 2",
booktitle = "Automata, Languages and Programming",
booksubtitle = "16th International Colloquium",
editor = "Ausiello, Giorgio and Dezani-Ciancaglini, Mariangiola and Ronchi della Rocca, Simona",
series = "Lecture Notes in Computer Science",
volume = "372",
publisher = "Springer-Verlag",
address = "Berlin",
year = "1989",
place = "Stresa, Italy",
dates = "July 11--15",
pages = "704--722",
comments = "same as REYNOLDS89A",
filename = "syncontrol2",
abstract = "In 1978, we proposed that Algol-like languages should be constrained
so that aliasing between variables and, more generally, interference between
commands or procedures would be syntactically detectable in a fail-safe
manner. In particular, we proposed syntactic restrictions that prohibited
interference between distinct identifiers, while permitting interference
between qualifications of the same identifier. However, these restrictions
had the unfortunate property that syntactic correctness was not preserved
by beta reduction.
In the present paper, we show how this difficulty can be avoided by
the use of a variant of conjunctive types. We also give an algorithm
for typechecking explicitly typed programs.",
checked = "18 July 1989"}
@techreport{REYNOLDS89A,
author = "Reynolds, John C.",
title = "Syntactic Control of Interference, Part 2",
type = "Report",
number = "CMU--CS--89--130",
institution = "Carnegie Mellon University",
department = "Computer Science Department",
address = "Pittsburgh, Pennsylvania",
month = "April 17,",
year = "1989",
comments = "same as REYNOLDS89",
filename = "syncontrol2",
abstract = "In 1978, we proposed that Algol-like languages should be constrained
so that aliasing between variables and, more generally, interference between
commands or procedures would be syntactically detectable in a fail-safe
manner. In particular, we proposed syntactic restrictions that prohibited
interference between distinct identifiers, while permitting interference
between qualifications of the same identifier. However, these restrictions
had the unfortunate property that syntactic correctness was not preserved
by beta reduction.
In the present paper, we show how this difficulty can be avoided by
the use of a variant of conjunctive types. We also give an algorithm
for typechecking explicitly typed programs.",
checked = "23 May 1989"}
@unpublished{REYNOLDS89B,
author = "Reynolds, John C.",
title = "Even Normal Forms Can be Hard to Type",
note = "Unpublished, marked Carnegie Mellon University",
month = "December 1,",
year = "1989",
address = "Pittsburgh, Pennsylvania 15213",
department = "Department of Computer Science",
filename = "normhard",
checked = "31 December, 1993"}
@incollection{REYNOLDS90,
author = "Reynolds, John C. and Plotkin, Gordon D.",
title = "On Functors Expressible in the Polymorphic Typed Lambda Calculus",
note = "A preliminary version of a paper to appear in Information and Computation",
booktitle = "Logical Foundations of Functional Programming",
editor = "G{\'e}rard Huet",
publisher = "Addison-Wesley",
address = "Reading, Massachusetts",
year = "1990",
pages = "127--152",
hidseries = "University of Texas at Austin Year of Programming",
comments = "in HUET90, same as REYNOLDS88 and superseded by REYNOLDS90B and REYNOLDS93B",
checked = "9 August 1990",
updated = "29 July 1993"}
@incollection{REYNOLDS90A,
author = "Reynolds, John C.",
title = "Introduction to Part {II}, Polymorphic Lambda Calculus",
booktitle = "Logical Foundations of Functional Programming",
editor = "G{\'e}rard Huet",
publisher = "Addison-Wesley",
address = "Reading, Massachusetts",
year = "1990",
pages = "77--86",
hidseries = "University of Texas at Austin Year of Programming",
comments = "in HUET90",
filename = "polyintro",
checked = "9 August 1990"}
@techreport{REYNOLDS90B,
author = "Reynolds, John C. and Plotkin, Gordon D.",
title = "On Functors Expressible in the Polymorphic Typed Lambda Calculus",
type = "Report",
number = "CMU--CS--90--147",
institution = "Carnegie Mellon University",
department = "School of Computer Science",
address = "Pittsburgh, Pennsylvania",
month = "July 6,",
year = "1990",
comments = "revision of REYNOLDS88 and REYNOLDS90, superceded by (but almost identical to) REYNOLDS93B",
updated = "29 July 1993",
checked = "9 August 1990"}
@inproceedings{REYNOLDS91,
author = "Reynolds, John C.",
title = "The Coherence of Languages with Intersection Types",
booktitle = "Theoretical Aspects of Computer Software",
booksubtitle = "International Conference TACS '91, Proceedings",
editor = "Takayasu Ito and Albert R. Meyer",
series = "Lecture Notes in Computer Science",
volume = "526",
publisher = "Springer-Verlag",
address = "Berlin",
year = "1991",
place = "Sendai, Japan",
dates = "September 24--27, 1991",
pages = "675--700",
filename = "coherence",
abstract = "When a programming language has a sufficiently rich type structure,
there can be more than one proof of the same typing judgement;
potentially this can lead to semantic ambiguity
since the semantics of a typed language is a function of such proofs.
When no such ambiguity arises, we say that the language is {\em coherent}.
In this paper we prove the coherence of a class of lambda-calculus-based
languages that use the intersection type discipline, including both
a purely functional programming language and the Algol-like
programming language Forsythe.",
checked = "31 October 1991"}
@inproceedings{REYNOLDS91A,
author = "Ma, QingMing and Reynolds, John C.",
title = "Types, Abstraction, and Parametric Polymorphism, Part 2",
booktitle = "Mathematical Foundations of Programming Semantics",
booksubtitle = "7th International Conference, Proceedings",
place = "Pittsburgh, Pennsylvania",
dates = "March 25--28, 1991",
editor = "Stephen D. Brookes and Michael Main and Austin Melton and Michael Mislove and David A. Schmidt",
series = "Lecture Notes in Computer Science",
volume = "598",
publisher = "Springer-Verlag",
address = "Berlin",
year = "1992",
pages = "1--40",
filename = "parpoly2",
abstract = "The concept of relations over sets is generalized to relations over
an arbitrary category, and used to investigate the abstraction (or logical-relations)
theorem, the identity extension lemma, and parametric polymorphism, for
Cartesian-closed-category models of the simply typed lambda calculus and PL-category
models of the polymorphic typed lambda calculus. Treatments of Kripke relations
and of complete relations on domains are included.",
checked = "17 August 1992"}
@unpublished{REYNOLDS91B,
author = "Reynolds, John C.",
title = "Replacing Complexity with Generality: The Programming Language {F}orsythe",
note = "Unpublished, marked Carnegie Mellon University, April 12",
year = "1991",
address = "Pittsburgh, Pennsylvania 15213",
department = "Department of Computer Science",
filename = "forsytheintro",
abstract = "By using concepts of modern programming-language theory, such as
higher-order procedures and intersection types, it is possible to
design a programming language that is extremely general without being
complicated. This thesis is illustrated by the Algol-like language
Forsythe.",
checked = "12 December, 1994"}
@inproceedings{REYNOLDS93,
author = "Reynolds, John C.",
title = "An Introduction to Logical Relations and Parametric Polymorphism (Tutorial)",
booktitle = "Conference Record of the Twentieth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages",
publisher = "ACM Press",
address = "New York",
note = "Abstract only",
dates = "January 10--13",
year = "1993",
place = "Charleston, South Carolina",
pages = "155--156",
updated = "1 December 1994",
checked = "9 February 1993"}
@article{REYNOLDS93B,
author = "Reynolds, John C. and Plotkin, Gordon D.",
title = "On Functors Expressible in the Polymorphic Typed Lambda Calculus",
journal = "Information and Computation",
month = "July",
volume = "105",
number = "1",
year = "1993",
pages = "1--29",
comments = "revision of REYNOLDS88, REYNOLDS90 and REYNOLDS90B, almost identical to REYNOLDS90B",
filename = "functexp",
abstract = "Given a model of the polymorphic typed lambda calculus based upon a
Cartesian closed category ${\cal K}$, there will be functors from ${\cal K}$ to
${\cal K}$ whose action on objects can be expressed by type expressions and whose
action on morphisms can be expressed by ordinary expressions. We show that if $T$
is such a functor then there is a weak initial $T$-algebra and if, in addition,
${\cal K}$ possesses equalizers of all subsets of its morphism sets, then there is
an initial $T$-algebra. These results are used to establish the impossibility of
certain models, including those in which types denote sets and $S\rightarrow S'$
denotes the set of all functions from $S$ to $S'$.",
checked = "29 July 1993"}
@article{REYNOLDS93C,
author = "Reynolds, John C.",
title = "The Discoveries of Continuations",
journal = "Lisp and Symbolic Computation",
volume = "6",
number = "3--4",
pages = "233--247",
month = "November",
year = "1993",
filename = "histcont",
url = "http://www.brics.dk/~hosc/local/LaSC-6-34-pp233-248.pdf",
abstract = "We give a brief account of the discoveries of continuations and related
concepts by A.~van Wijngaarden, A.~W.~Mazurkiewicz, F.~L.~Morris, C.~P.~Wadsworth,
J.~H.~Morris, M.~J.~Fischer, and S.~K.~Abdali.",
checked = "3 January 1994"}
@inproceedings{REYNOLDS94,
author = "Reynolds, John C.",
title = "Using Functor Categories to Generate Intermediate Code",
booktitle = "Conference Record of POPL '95: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages",
publisher = "ACM Press",
address = "New York",
dates = "January 22--25",
year = "1995",
place = "San Francisco",
pages = "25--36",
reprint = "Reprinted in \authorcite{O'Hearn and Tennent} \crosscite[vol.~2, pages~13--38]{OHEARN97}",
filename = "intcode",
abstract = "In the early 80's Oles and Reynolds devised a semantic model of
Algol-like languages using a category of functors from a category of store
shapes to the category of predomains. Here we will show how a variant of
this idea can be used to define the translation of an Algol-like language to
intermediate code in a uniform way that avoids unnecessary temporary variables,
provides control-flow translation of boolean expressions, permits online
expansion of procedures, and minimizes the storage overhead of calls of
closed procedures. The basic idea is to replace continuations by instruction
sequences and store shapes by descriptions of the structure of the run-time
stack.",
checked = "24 February 1995",
updated = "10 May 1997"}
@techreport{REYNOLDS96,
author = "Reynolds, John C.",
title = "Design of the Programming Language {F}orsythe",
type = "Report",
number = "CMU--CS--96--146",
institution = "Carnegie Mellon University",
department = "School of Computer Science",
address = "Pittsburgh, Pennsylvania",
month = "June 28,",
year = "1996",
reprint = "Reprinted in \authorcite{O'Hearn and Tennent} \crosscite[vol.~1, pages~173--233]{OHEARN97}",
comments = "supersedes REYNOLDS88B",
filename = "forsytherep",
abstract = "This is a description of the programming language Forsythe, which is
a descendant of Algol 60 intended to be as uniform and general as possible,
while retaining the basic character of its progenitor.",
checked = "28 June 1996",
updated = "10 May 1997"}
@article{REYNOLDS96B,
author = "Reynolds, John C.",
title = "Beyond ML",
journal = "ACM Computing Surveys (electronic)",
url = "http://www.acm.org/pubs/citations/journals/surveys/1996-28-4es/a172-reynolds/",
volume = "28",
number = "4es",
month = "December",
pages = "172--es",
year = "1996",
filename = "beyondml",
abstract = "We believe that the most pressing problem in programming-language design
is to control the interference that arises when functional and imperative
programming are combined, and to give the user more control of storage
allocation, without sacrificing the virtues of higher-order procedures,
rigorous typing, and modularity that characterize ML. Towards this end,
we intend to pursue research on Algol-like languages, linear typing,
and the use of regions for storage allocation.",
entered = "27 May 1998"}
@inproceedings{REYNOLDS98,
author = "Reynolds, John C.",
title = "Where Theory and Practice Meet: POPL Past and Future",
booktitle = "Conference Record of POPL '98: The 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages",
publisher = "ACM Press",
address = "New York",
dates = "January 19--21",
year = "1998",
place = "San Diego",
note = "There is no textual version of this talk, but the slides are available on the Internet",
url = "http://www.luca.demon.co.uk/POPL98/InvitedTalks.html",
checked = "28 May 1998"}
@inproceedings{REYNOLDS98B,
author = "Reynolds, John C.",
title = "Normalization and Functor Categories",
booktitle = "Preliminary Proceedings of the 1998 APPSEM Workshop on Normalization by Evaluation NBE '98",
editor = "Olivier Danvy and Peter Dybjer",
place = "Gothenburg, Sweden",
dates = "May 8--9",
year = "1998",
series = "BRICS Note Series",
number = "NS--98--1",
department = "Department of Computer Science",
institution = "University of Aarhus",
address = "Aarhus, Denmark",
pages = "24--27",
filename = "normfuncat",
abstract = "There is a functor-category model of the simply typed
lambda calculus such that the long $\beta$-$\eta$-normal form of any
expression can be obtained from its meaning.",
checked = "28 May 1998"}
@book{REYNOLDS98C,
author = "Reynolds, John C.",
title = "Theories of Programming Languages",
publisher = "Cambridge University Press",
address = "Cambridge, England",
year = "1998",
pages = "xii+500",
isbn = "9780521594141 (hardback), 0-521-59414-6 (old hardback), 9780521106979 (paperback, Spring 2009)",
callno = "QA76.7.R495 1998",
checked = "6 October 1998",
updated = "6 October 2009"}
@article{REYNOLDS98D,
author = "Reynolds, John C.",
title = "Definitional Interpreters for Higher-Order Programming Languages",
journal = "Higher-Order and Symbolic Computation",
volume = "11",
number = "4",
pages = "363--397",
month = "December",
year = "1998",
filename = "defint",
url = "http://www.brics.dk/~hosc/local/HOSC-11-4-pp363-397.pdf",
abstract = "Higher-order programming languages (i.e., languages in which procedures
or labels can occur as values) are usually defined by interpreters that are
themselves written in a programming language based on the lambda calculus (i.e., an
applicative language such as pure LISP). Examples include McCarthy's definition
of LISP, Landin's SECD machine, the Vienna definition of PL/I, Reynolds'
definitions of GEDANKEN, and recent unpublished work by L. Morris and
C. Wadsworth. Such definitions can be classified according to whether the
interpreter contains higher-order functions, and whether the order of
application (i.e., call by value versus call by name) in the defined language
depends upon the order of application in the defining language. As an example,
we consider the definition of a simple applicative programming language by
means of an interpreter written in a similar language. Definitions in each
of the above classifications are derived from one another by informal but
constructive methods. The treatment of imperative features such as jumps and
assignment is also discussed.",
comments = "Reprint of REYNOLDS72A",
checked = "25 January 1999"}
@article{REYNOLDS98E,
author = "Reynolds, John C.",
title = "Definitional Interpreters Revisited",
journal = "Higher-Order and Symbolic Computation",
volume = "11",
number = "4",
pages = "355--361",
month = "December",
year = "1998",
filename = "defintintro",
url = "http://www.brics.dk/~hosc/local/HOSC-11-4-pp355-361.pdf",
abstract = "To introduce the republication of ``Definitional Interpreters for
Higher-Order Programming Languages'', the author recounts the circumstances of its
creation, clarifies several obscurities, corrects a few mistakes, and briefly
summarizes some more recent developments.",
comments = "Introduction to REYNOLDS98D",
checked = "25 January 1999"}
@unpublished{REYNOLDS99,
author = "Reynolds, John C.",
title = "Reasoning about Shared Mutable Data Structure (Preliminary Version)",
note = "Appeared in the preliminary proceedings of the Symposium in Celebration of the Work of C. A. R. Hoare (St. Catherine's College, Oxford, 13th--15th September 1999.) This version contained a serious error that was corrected in the revised version \cite{REYNOLDS00}.",
month = "August 12,",
year = "1999",
abstract = "Drawing on early work by Burstall, we extend Hoare's
approach to the partial correctness of imperative programs to deal
with programs that perform destructive updates to data structures
containing more than one pointer to the same location. The key
concept is an ``independent conjunction'' P & Q, which only holds
when P and Q are both true and depend upon distinct areas of
storage. Exemplary proofs are given of simple programs that
manipulate singly and doubly linked lists.",
entered = "13 August 1999",
updated = "1 February 2000"}
@inproceedings{REYNOLDS00,
author = "Reynolds, John C.",
title = "Intuitionistic Reasoning about Shared Mutable Data Structure",
year = "2000",
booktitle = "Millennial Perspectives in Computer Science",
booksubtitle = "Proceedings of the 1999 Oxford--Microsoft Symposium in Honour of Sir Tony Hoare",
editor = "Jim Davies and Bill Roscoe and Jim Woodcock",
publisher = "Palgrave",
address = "Houndsmill, Hampshire",
comments = "Supercedes REYNOLDS99",
isbn = "0-333-92230-1",
pages = "303--321",
filename = "shareddata",
abstract = "Drawing upon early work by Burstall, we extend Hoare's approach
to proving the correctness of imperative programs, to deal with programs
that perform destructive updates to data structures containing more than
one pointer to the same location. The key concept is an ``independent
conjunction'' P & Q that holds only when P and Q are both true and depend
upon distinct areas of storage. To make this concept precise we use an
intuitionistic logic of assertions, with a Kripke semantics whose possible
worlds are heaps (mapping locations into tuples of values).",
checked = "12 December 2000"}
@inproceedings{REYNOLDS00B,
author = "Reynolds, John C.",
title = "An Intrinsic Semantics of Intersection Types (Abstract of Invited Lecture)",
booktitle = "Proceedings of the Workshop on Intersection Types and Related Systems",
dates = "July 15",
year = "2000",
place = "Geneva, Switzerland",
comments = "The file named below contains the slides used for the lecture",
note = "The slides for this lecture are available at ftp://ftp.cs.cmu.edu/user/jcr/intertype.ps.gz",
filename = "intertype",
abstract = "Most models of intersection types, such as filter models, are
extrinsic semantics, i.e., terms have the same meaning as in a typeless model,
and the type of a term denotes a property of its meaning. In contrast, the
usual denotational semantics of a real programming languages is an intrinsic
semantics, in which only well-typed terms have meanings, which are defined by
induction on the proof of their typing.",
entered = "28 July 2000"}
@unpublished{REYNOLDS00C,
author = "Reynolds, John C.",
title = "Lectures on Reasoning about Shared Mutable Data Structure",
note = "{\rm IFIP Working Group 2.3 School/Seminar on State-of-the-Art Program Design Using Logic, Tandil, Argentina, September 6-13}",
year = "2000",
comments = "The file named below contains the slides used for the lecture",
filename = "tandilslides",
abstract = "The topic of these lectures is an extension of Hoare logic to
the specification and proof of programs in which data structures can contain
several pointers to the same location, whose contents can be modified by the
program. It is based on recent work by the author, and by Samin Ishtiaq and
Peter W. O'Hearn.",
entered = "21 September 2000"}
@inproceedings{REYNOLDS01,
author = "Reynolds, John C. and O'Hearn, Peter W.",
title = "Reasoning About Shared Mutable Data Structure (Abstract of Invited Lecture)",
booktitle = "SPACE 2001: Informal Proceedings of Workshop on Semantics, Program Analysis and Computing Environments for Memory Management",
editor = "Fritz Henglein and John Hughes and Henning Makholm and Henning Niss",
dates = "January 15--16",
year = "2001",
place = "London",
publisher = "IT University of Copenhagen",
pages = "7",
comments = "The file named below contains the slides used for the lecture",
note = "The slides for this lecture are available at ftp://ftp.cs.cmu.edu/user/jcr/spacetalk.ps.gz",
filename = "spacetalk",
abstract = "We describe an extension of Hoare logic to permit reasoning about
shared mutable data structure.
The simple imperative language is extended with commands (not
expressions) for accessing and modifying shared mutable structures,
and with nondetermininstic allocation, explicit deallocation, and
unrestricted address arithmetic. Semantically, this extension
involves separating the state of the computation into a store
that maps variables into integers, and a heap that maps locations
(a subset of the integers) into integers.
Assertions are extended by introducing an independent conjunction
operation that asserts that its subformulas hold for disjoint
parts of the heap. Coupled with the inductive definition of
predicates on abstract data structures, this extension permits
the concise and flexible description of data structures with
controlled sharing.
Although address arithmetic is unrestricted, the nondeterminacy
of storage allocation insures that valid specifications never
describe programs that violate record or array boundaries.",
checked = "23 January 2001"}
@techreport{REYNOLDS01B,
author = "Reynolds, John C.",
title = "The Meaning of Types --- From Intrinsic to Extrinsic Semantics",
year = "2000",
month = "December",
type = "Research Series",
number = "RS--00--32",
institution = "BRICS",
address = "DAIMI, Department of Computer Science, University of Aarhus",
comments = "REYNOLDS01C is a shorter version of this paper describing a more limited language",
note = "http://www.brics.dk/RS/00/32/",
filename = "typemeaning",
abstract = "A definition of a typed language is said to be ``intrinsic''
if it assigns meanings to typings rather than arbitrary phrases, so that
ill-typed phrases are meaningless. In contrast, a definition is said
to be ``extrinsic'' if all phrases have meanings that are independent
of their typings, while typings represent properties of these meanings.
For a simply typed lambda calculus, extended with recursion,
subtypes, and named products, we give an intrinsic denotational semantics
and a denotational semantics of the underlying untyped language. We then
establish a logical relations theorem between these two semantics, and show
that the logical relations can be ``bracketed'' by retractions between
the domains of the two semantics. From these results, we derive an extrinsic
semantics that uses partial equivalence relations.
A definition of a typed language is said to be ``intrinsic'' if it assigns
meanings to typings rather than arbitrary phrases, so that ill-typed phrases
are meaningless. In contrast, a definition is said to be ``extrinsic''
if all phrases have meanings that are independent of their typings, while
typings represent properties of these meanings.
For a simply typed lambda calculus, extended with recursion, subtypes,
and named products, we give an intrinsic denotational semantics and a
denotational semantics of the underlying untyped language. We then
establish a logical relations theorem between these two semantics, and show
that the logical relations can be ``bracketed'' by retractions between
the domains of the two semantics. From these results, we derive an
extrinsic semantics that uses partial equivalence relations.",
checked = "18 February 2001"}
@incollection{REYNOLDS01C,
author = "Reynolds, John C.",
title = "What do Types Mean? --- From Intrinsic to Extrinsic Semantics",
booktitle = "Essays on Programming Methodology",
editor = "Annabelle McIver and Carroll Morgan",
publisher = "Springer-Verlag",
address = "New York",
year = "2002",
comments = "REYNOLDS01B is a longer version of this paper describing a more elaborate language",
filename = "shorttypemeaning",
abstract = "A definition of a typed language is said to be ``intrinsic'' if it
assigns meanings to typings rather than arbitrary phrases, so that ill-typed
phrases are meaningless. In contrast, a definition is said to be
``extrinsic'' if all phrases have meanings that are independent of their
typings, while typings represent properties of these meanings.
For a simply typed lambda calculus, extended with integers, recursion, and
conditional expressions, we give an intrinsic denotational semantics and a
denotational semantics of the underlying untyped language. We then
establish a logical relations theorem between these two semantics, and show
that the logical relations can be ``bracketed'' by retractions between
the domains of the two semantics. From these results, we derive an extrinsic
semantics that uses partial equivalence relations.",
entered = "8 February 2001",
updated = "24 September 2004"}
@inproceedings{REYNOLDS02,
author = "Reynolds, John C.",
title = "Separation Logic: A Logic for Shared Mutable Data Structures",
booktitle = "Proceedings Seventeenth Annual IEEE Symposium on Logic in Computer Science",
publisher = "IEEE Computer Society",
address = "Los Alamitos, California",
dates = "July 22--25",
year = "2002",
place = "Copenhagen, Denmark",
pages = "55--74",
filename = "seplogic",
abstract = "In joint work with Peter O'Hearn and others, based on early
ideas of Burstall, we have developed an extension of Hoare logic
that permits reasoning about low-level imperative programs that
use shared mutable data structure.
The simple imperative programming language is extended with commands
(not expressions) for accessing and modifying shared structures, and
for explicit allocation and deallocation of storage. Assertions are
extended by introducing a ``separating conjunction'' that asserts that
its subformulas hold for disjoint parts of the heap, and a closely
related ``separating implication''. Coupled with the inductive
definition of predicates on abstract data structures, this extension
permits the concise and flexible description of structures with
controlled sharing.
In this paper, we will survey the current development of this program
logic, including extensions that permit unrestricted address arithmetic,
dynamically allocated arrays, and recursive procedures. We will also
discuss promising future directions.",
entered = "9 May 2002"}
@inproceedings{REYNOLDS04,
author = "Reynolds, John C.",
title = "Towards a Grainless Semantics for Shared Variable Concurrency (abstract only)",
booktitle = "Conference Record of POPL 2004: The 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages",
publisher = "ACM Press",
address = "New York",
dates = "January 14--16",
year = "2004",
place = "Venice, Italy",
comment = "Superceded by REYNOLDS04C",
filename = "grainlesstalk",
comments = "SIGPLAN Programming Language Achievement Award Lecture. There is no textual version of this talk, but the slides are available on the Internet",
url = "http://www.cs.cmu.edu/\verb+~+jcr",
abstract = "Conventional semantics for shared variable concurrency
imposes a default choice of the level of atomicity that is often
unrealistic for an actual implementation - this is commonly
called the `grain of time' phenomenon. We propose a semantics
that avoids any such choice. It is based on three principles:
- All operations have duration and can overlap one another
during execution.
- If two overlapping operations touch the same location, the
meaning of the program execution is `wrong'.
- If, from a given starting state, execution of a program can
give `wrong', then no other possibilities need be considered.",
checked = "31 January 2004",
updated = "10 September 2004"}
@unpublished{REYNOLDS04B,
author = "Reynolds, John C.",
title = "Types, Abstraction, and Parametric Polymorphism --- For Domains",
note = "Unpublished slides for Mathematical Foundations of Programming Language Semantics, 20th Workshop",
place = "Carnegie Mellon University, Pittsburgh, Pennsylvania",
dates = "May 23, 2004",
filename = "parpolydom",
abstract = "When domains are used to model parametric polymorphism,
the principle of parametricity (roughly speaking, that polymorphic
functions ``behave'' the same way for all types) permits one to
determine many polymorphic domains explicitly. We will explore
some interesting examples, including the paradoxical type that
cannot be modelled in a set-theoretic semantics.",
checked = "11 June 2004"}
@inproceedings{REYNOLDS04C,
author = "Reynolds, John C.",
title = "Toward a Grainless Semantics for Shared-Variable Concurrency",
booktitle = "FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science",
booksubtitle = "24th International Conference, Proceedings",
editor = "Kamal Lodaya and Meena Mahajan",
series = "Lecture Notes in Computer Science",
volume = "3328",
publisher = "Springer-Verlag",
address = "Berlin",
dates = "December 16--18",
year = "2004",
place = "Chennai, India",
pages = "35--48",
comment = "Supercedes REYNOLDS04",
filename = "grainless",
abstract = "Conventional semantics for shared-variable concurrency
suffers from the ``grain of time'' problem, i.e., the necessity
of specifying a default level of atomicity. We propose a semantics
that avoids any such choice by regarding all interference that is
not controlled by explicit critical regions as catastrophic.
It is based on three principles:
--- Operations have duration and can overlap one another
during execution.
--- If two overlapping operations touch the same location, the
meaning of the program execution is ``wrong''.
--- If, from a given starting state, execution of a program can
give ``wrong'', then no other possibilities need be considered.",
checked = "18 February 2005",
updated = "1 August 2005"}
@unpublished{REYNOLDS05,
author = "Reynolds, John C.",
title = "Precise, Intuitionistic, and Supported Assertions in Separation Logic",
note = "Unpublished slides for Mathematical Foundations of Programming Language Semantics, 21th Workshop",
place = "University of Birmingham, England",
dates = "May 21",
year = "2005",
filename = "pisaseplog",
abstract = "These classes of assertions, which are defined semantically,
play a special role in several aspects of separation logic. They allow
one to use a full distributive law between ordinary and separating
conjunction. They suffice for the soundness of the hypothetical frame
rule and O'Hearn's rules for shared-variable concurrency with conditional
critical regions. Precise assertions also indicate the absence of memory
leaks.",
checked = "14 June 2005"}
@unpublished{REYNOLDS05B,
author = "Reynolds, John C.",
title = "Further Towards a Grainless Semantics for Shared Variable Concurrency",
note = "Invited Talk at FMCO 2005 (no text or copies of slides available)",
place = "Amsterdam",
dates = "November 3",
year = "2005",
checked = "27 November 2005"}
@inproceedings{REYNOLDS05C,
author = "Reynolds, John C.",
title = "An Overview of Separation Logic",
booktitle = "Verified Software: Theories, Tools, Experiments",
editor = "Bertrand Meyer and Jim Woodcock",
series = "Lecture Notes in Computer Science",
volume = "4171",
publisher = "Springer-Verlag",
address = "Berlin",
dates = "October 2005",
year = "2008",
place = "Zurich, Switzerland",
pages = "460-469",
filename = "seplogoverview",
abstract = "After some general remarks about program verification,
we introduce separation logic, a novel extension of Hoare logic than can
strengthen the applicability and scalability of program verification for
imperative programs using shared mutable data structures or shared-memory
concurrency.",
entered = "19 February 2009"}
@unpublished{REYNOLDS07,
author = "Reynolds, John C.",
title = "Grainless Semantics without Critical Regions",
note = "Unpublished slides for Mathematical Foundations of Programming Language Semantics, 23rd Annual Conference (in session honoring Gordon Plotkin's 60th birthday)",
place = "Tulane University, New Orleans",
dates = "April 11",
year = "2007",
filename = "grainlesswcrtalk",
abstract = "We develop a grainless semantics for shared-variable
concurrency in the absence of critical regions, allocation or
deallocation, and passivity. Surprisingly, concurrency does not lead to
nondeterminism. (Work in progress jointly with Ruy Ley-Wild)",
checked = "21 October 2007"}
@article{REYNOLDS08,
author = "Reynolds, John C.",
title = "Some Thoughts on Teaching Programming and Programming Languages",
booktitle = "Proceedings of the SIGPLAN Programming Language Curriculum Workshop",
place = "Harvard University, Cambridge, Massachusetts",
dates = "May 29--30, 2008",
journal = "SIGPLAN Notices",
month = "November",
year = "2008",
volume = "43",
number = "11",
pages = "108--110",
filename = "plcurr",
abstract = "It is argued that the teaching of programming is central to the
education of skilled computer professionals, that the teaching of programming
languages is central to the teaching of programming. that these topics must
include the specification, structuring, and verification of software, and that
they should be taught with the same regard to rigor and precision as in
traditional mathematics.",
entered = "20 June 2008",
updated = "19 February 2009"}
@unpublished{REYNOLDS08A,
author = "Reynolds, John C.",
title = "A Problematic Program (Joint work with Josh Berdine)",
note = "Unpublished slides for a talk at the Dagstuhl Seminar on Types, Logic, and Semantics for State",
place = "Dagstuhl, Germany",
dates = "February 5",
year = "2008",
filename = "probprog",
entered = "10 July 2011"}
@unpublished{REYNOLDS08B,
author = "Reynolds, John C.",
title = "Readable Formal Proofs",
note = "Unpublished slides for an invited talk at Verified Software: Theories, Tools, Experiments, Second International Conference, VSTTE 2008",
place = "Toronto, Canada",
dates = "October 6--9",
year = "2008",
comment = "Superceded by REYNOLDS09",
filename = "readproofs",
abstract = "The need to integrate the processes of programming and program
verification requires notations for formal proofs that are easily
readable. We discuss this problem in the context of Hoare logic and
separation logic.
It has long been the custom to describe formal proofs in these logics
informally by means of `annotated specifications' or `proof outlines'. For
simple programs, these annotated specifications are essentially similar to
the annotated flow charts introduced by Floyd and Naur. For more
elaborate programs, a richer notation has evolved for dealing with
procedure calls and various structural rules, such as the frame axiom, as
well as various rules for concurrency.
Our goal is to devise a formalism for insuring that annotated
specifications actually determine valid formal proofs (modulo the
correctness of verification conditions), while providing as much
flexibility as possible. For this purpose, we give inference rules for
`annotation definitions' that assert that an annotated specification
determines a particular Hoare triple.",
entered = "15 December 2008",
updated = "10 July 2011"}
@unpublished{REYNOLDS09,
author = "Reynolds, John C.",
title = "Readable Proofs in Hoare Logic and Separation Logic",
note = "Unpublished slides for an invited talk at ETAPS 2009",
place = "York, England",
dates = "March 25",
year = "2009",
comment = "Supercedes REYNOLDS08B",
filename = "readproofshlsl",
entered = "10 July 2011"}
@unpublished{REYNOLDS11,
author = "Reynolds, John C.",
title = "Automatic Computation of Static Variable Permissions",
note = "Unpublished slides for an invited talk at Mathematical Foundations of Programming Language Semantics, 27th Annual Conference",
place = "Pittsburgh",
dates = "May 25--28",
year = "2011",
filename = "autovarperm",
abstract = "We will describe a procedure for inferring permissions for the
proof system described by Uday S. Reddy in an earlier talk at this conference.
Given a purported proof in Reddy's formalism in which the variable permissions
have been erased, our goal is to determine if there is an assignment of
permissions that will give a valid proof.",
entered = "10 July 2011"}
@unpublished{REYNOLDS11B,
author = "Reynolds, John C.",
title = "Making Program Logics Intelligible",
note = "Unpublished slides for the Lovelace Lecture",
place = "London",
dates = "June 8",
year = "2011",
filename = "lovelace",
abstract = "To verify program specifications, rather than generic safety properties,
it will be necessary to integrate verification into the process of programming.
Program proving is unlike theorem proving in mathematics - mathematical
conjectures may give no hint as to how they could be proved, but programs
are written by programmers, who must understand informally why their
programs work. The job of verification is not to explore some immense
search space, but to formalize the programmer's intuitions until any faults
are revealed.
This requires specifications and proofs that are succinct and intelligible
- which in turn require logics that go beyond predicate calculus (the
assembly language of program proving). In this talk, I will recount and
illustrate several steps, old and new, towards this goal, including interval
and partition diagrams, lacy arrays, and separation logic.",
entered = "10 July 2011"}
@inproceedings{TORPSMITH04,
author = "Birkedal, Lars and Torp-Smith, Noah and Reynolds, John C.",
title = "Local Reasoning about a Copying Garbage Collector",
booktitle = "Conference Record of POPL 2004: The 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages",
publisher = "ACM Press",
address = "New York",
dates = "January 14--16",
year = "2004",
place = "Venice, Italy",
pages = "220--231",
comments = "Superceded by TORPSMITH08",
filename = "copygarbcoll",
abstract = "We present a programming language, model, and logic appropriate
for implementing and reasoning about a memory management system. We then
state what is meant by correctness of a copying garbage collector, and
employ a variant of the novel separation logics to formally specify
correctness of Cheney's copying garbage collector. Finally, we prove that
our implementation of Cheney's algorithm meets its specification, using the
logic we have given, and auxiliary variables.",
checked = "31 January 2004"}
@article{TORPSMITH08,
author = "Torp-Smith, Noah and Birkedal, Lars and Reynolds, John C.",
title = "Local Reasoning about a Copying Garbage Collector",
journal = "ACM Transactions on Programming Languages and Systems",
volume = "30",
number = "4",
pages = "24:1--58",
comments = "Supercedes TORPSMITH04",
year = "2008",
abstract = "We present a programming language, model, and logic appropriate
for implementing and reasoning about a memory management system. We state
semantically what is meant by correctness of a copying garbage collector,
and employ a variant of the novel separation logics to formally specify
partial correctness of Cheney's copying garbage collector in our program
logic. Finally we prove that our implementation of Cheney's algorithm meets
its specification using the logic we have given and auxilliary variables.",
checked = "15 December 2008"}