SannellaDT.bib

@INPROCEEDINGS{SannellaDT:implementations82,
  AUTHOR = {Donald Sannella and Martin Wirsing},
  TITLE = {Implementation of Parameterised Specifications},
  BOOKTITLE = {Proc.\ 9th Intl.\ Colloq.\ on Automata, Languages
		 and Programming},
  LOCATION = {Aarhus},
  PUBLISHER = {Springer},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = 140,
  PAGES = {473--488},
  YEAR = 1982,
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/icalp82.pdf},
  ABSTRACT = {A new notion is given for the \emph{implementation} of one
specification by another.  Unlike most previous notions, this
generalises to handle parameterised specifications as well as
\emph{loose} specifications (having an assortment of non-isomorphic
models).  Examples are given to illustrate the notion.  The definition
of implementation is based on a new notion of the \emph{simulation}
of a theory by an algebra.  For the bulk of the paper we employ a
variant of the Clear specification language [BG77] in which the notion
of a \emph{data constraint} is replaced by the weaker notion of a
\emph{hierarchy constraint}.  All results hold for Clear with data
constraints as well, but only under more restrictive conditions.

We prove that implementations compose \emph{vertically} (two
successive implementation steps compose to give one large step) and
that they compose \emph{horizontally} under application of
(well-behaved) parameterised specifications (separate implementations
of the parameterised specification and the actual parameter compose to
give an implementation of the application).},
  COMMENT = {[Long version: Report CSR-103-82, Dept. of Computer
		 Science, Univ. of Edinburgh, 1982; reviewed in
		 Zbl 492.68023.]}
}

@PHDTHESIS{SannellaDT:phd82,
  AUTHOR = {Donald Sannella},
  TITLE = {Semantics, Implementation and Pragmatics of {C}lear,
		 a Program Specification Language},
  SCHOOL = {Department of Computer Science, University of Edinburgh},
  YEAR = 1982,
  ABSTRACT = {Specifications are necessary for communicating decisions and
intentions and for documenting results at many stages of the program
development process.  Informal specifications are typically used
today, but they are imprecise and often ambiguous.  Formal
specifications are precise and exact but are more difficult to write
and understand.  We present work aimed toward enabling the practical
use of formal specifications in program development, concentrating on
the Clear language for structured algebraic specification.

Two different but equivalent denotational semantics for Clear are
given.  One is a version of a semantics due to Burstall and Goguen
with a few corrections, in which the category-theoretic notion of a
colimit is used to define Clear's structuring operations independently
of the underlying ``institution'' (logical formalism).  The other
semantics defines the same operations by means of straightforward
set-theoretic constructions; it is not institution-independent but it
can be modified to handle all institutions of apparent interest.

Both versions of the semantics have been implemented.  The
set-theoretic implementation is by far the more useful of the two, and
includes a parser and typechecker.  An implementation is useful for
detecting syntax and type errors in specifications, and can be used as
a front end for systems which manipulate specifications.  Several
large specifications which have been processed by the set-theoretic
implementation are presented.

A semi-automatic theorem prover for Clear built on top of the
Edinburgh LCF system is described.  It takes advantage of the
structure of Clear specifications to restrict the available
information to that which seems relevant to proving the theorem at
hand.  If the system is unable to prove a theorem automatically the
user can attempt the proof interactively using the high-level
primitives and inference rules provided.

We lay a theoretical foundation for the use of Clear in systematic
program development by investigating a new notion of the
implementation of a specification by a lower-level specification.
This notion extends to handle parameterised specifications.  We show
that this implementation relation is transitive and commutes with
Clear's structuring operations under certain conditions.  This means
that a large specification can be refined to a program in a gradual
and modular fashion, where the correctness of the individual
refinements guarantees the correctness of the resulting program.},
  NOTE = {Report CST-17-82}
}

@INPROCEEDINGS{SannellaDT:structured-theories83,
  AUTHOR = {Donald Sannella and Rod Burstall},
  TITLE = {Structured Theories in {LCF}},
  BOOKTITLE = {Proc.\ 8th Colloq.\ on Trees in Algebra and
		 Programming},
  LOCATION = {L'Aquila},
  PUBLISHER = {Springer},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = 159,
  PAGES = {377--391},
  YEAR = 1983,
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/caap83.pdf},
  ABSTRACT = {An extension to the Edinburgh LCF interactive theorem-proving system
is described which provides new ways of constructing theories, drawing
upon ideas from the Clear specification language.  A new theory can be
built from an existing theory in two new ways: by \emph{renaming} its
types and constants, or by \emph{abstraction} (forgetting some types
and constants and perhaps renaming the rest).  A way of providing
\emph{parameterised} theories is described.  These theory-building
operations --- together with operations for forming a \emph{primitive}
theory and for taking the \emph{union} of theories --- allow large
theories to be built in a flexible and well-structured fashion.
Inference rules and strategies for proof in structured theories are
also discussed.}
}

@INPROCEEDINGS{SannellaDT:asl83,
  AUTHOR = {Donald Sannella and Martin Wirsing},
  TITLE = {A Kernel Language for Algebraic Specification and
		 Implementation},
  BOOKTITLE = {Proc.\ 1983 Intl.\ Conf.\ on Foundations of
		 Computation Theory},
  LOCATION = {Borgholm},
  YEAR = 1983,
  COMMENT = {[Long version: Report CSR-131-83, Dept. of Computer
		 Science, Univ. of Edinburgh, 1983.]},
  PAGES = {413--427},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = 158,
  PUBLISHER = {Springer},
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/asl.pdf},
  ABSTRACT = {A kernel specification language called ASL is presented.  ASL
comprises five fundamental but powerful specification-building
operations and has a simple semantics.  Behavioural abstraction with
respect to a set of observable sorts can be expressed, and (recursive)
parameterised specifications can be defined using a more powerful and
more expressive parameterisation mechanism than usual.  A simple
notion of implementation permitting vertical and horizontal
composition (i.e. it is transitive and monotonic) is adopted and
compared with previous more elaborate notions.  A collection of
identities is given which can provide a foundation for the development
of programs by transformation.}
}

@INPROCEEDINGS{SannellaDT:behavioural-abstraction83,
  AUTHOR = {Donald Sannella},
  TITLE = {Behavioural Abstraction and Algebraic Specification},
  PAGES = {153--166},
  BOOKTITLE = {Proc.\ 1983 Workshop on Semantics of Programming
		 Languages},
  LOCATION = {G{\"}oteborg},
  YEAR = 1983,
  ABSTRACT = {We argue that a proper notion of behavioural equivalence (a relation
on algebras) is fundamental to the theory of program
development.  This view is supported by arguments from abstract data
types, from program specification, and from stepwise refinement.  Many
different definitions of behavioural equivalence have appeared in the
literature, but each definition yields one of three relations which
differ only in their treatment of algebras containing unreachable data
elements.  Such algebras can be of use and so we adopt the relation
which seems to treat them properly.}
}

@ARTICLE{SannellaDT:clear-semantics84,
  AUTHOR = {Donald Sannella},
  TITLE = {A Set-Theoretic Semantics for {C}lear},
  JOURNAL = {Acta Informatica},
  VOLUME = 21,
  PAGES = {443--472},
  YEAR = 1984,
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/clear-semantics.pdf},
  ABSTRACT = {A semantics for the Clear specification language is given.  The
language of set theory is employed to present constructions
corresponding to Clear's specification-combining operations, which are
then used as the basis for a denotational semantics.  This is in
contrast to Burstall and Goguen's 1980 semantics which described the
meanings of these operations more abstractly via concepts from
category theory.},
  COMMENT = {[An early version is: A new semantics for {C}lear,
		 Report CSR-79-81, Dept. of Computer Science, Univ. of
		 Edinburgh, 1981.]}
}

@INPROCEEDINGS{SannellaDT:specs-arbitrary-institution84,
  AUTHOR = {Donald Sannella and Andrzej Tarlecki},
  TITLE = {Building Specifications in an Arbitrary Institution},
  BOOKTITLE = {Proc.\ Intl.\ Symp.\ on Semantics of Data Types},
  LOCATION = {Sophia-Antipolis},
  PUBLISHER = {Springer},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = 173,
  PAGES = {337--356},
  YEAR = 1984,
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/inst-asl-conf.pdf},
  NOTE = {\textbf{An extended and improved version is \cite{SannellaDT:specs-arbitrary-institution88}}},
  ABSTRACT = {A set of operations for constructing algebraic specifications in an
arbitrary logical system is presented. This builds on the framework
provided by Goguen and Burstall's work on the notion of an institution
as a formalisation of the concept of a logical system for writing
specifications. We show how to introduce free variables into the
sentences of an arbitrary institution and how to add quantifiers which
bind them. We use this foundation to define a set of primitive
operations for building specifications in an arbitrary institution
based loosely on those in the ASL kernel specification language, We
examine the set of operations which results when the definitions are
instantiated in an institution of first-order logic and compare these
with the operations found in existing specification languages. The
result of instantiating the operations in an institution of partial
first-order logic is also discussed,},
  COMMENT = {[Reviewed in CR 8505-0419.]}
}

@ARTICLE{SannellaDT:specs-arbitrary-institution88,
  AUTHOR = {Donald Sannella and Andrzej Tarlecki},
  TITLE = {Specifications in an Arbitrary Institution},
  JOURNAL = {Information and Computation},
  VOLUME = 76,
  PAGES = {165--210},
  YEAR = 1988,
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/inst-asl.pdf},
  ABSTRACT = {A formalism for constructing and using axiomatic specifications in an
arbitrary logical system is presented.  This builds on the framework
provided by Goguen and Burstall's work on the notion of an
\emph{institution} as a formalisation of the concept of a logical
system for writing specifications.  We show how to introduce free
variables into the sentences of an arbitrary institution and how to
add quantifiers which bind them.  We use this foundation to define a
set of primitive operations for building specifications in an
arbitrary institution based loosely on those in the ASL kernel
specification language.  We examine the set of operations which
results when the definitions are instantiated in institutions of total
and partial first-order logic and compare these with the operations
found in existing specification languages.  We present proof rules
which allow proofs to be conducted in specifications built using the
operations we define.  Finally, we introduce a simple mechanism for
defining and applying parameterised specifications and briefly discuss
the program development process.},
  COMMENT = {[Reviewed in MR 89d:68056 and Zbl 654.68017;
		 an early short version was
		 \cite{SannellaDT:specs-arbitrary-institution84}.]}
}

@INPROCEEDINGS{SannellaDT:thoughts85,
  AUTHOR = {Donald Sannella and Andrzej Tarlecki},
  TITLE = {Some Thoughts on Algebraic Specification},
  BOOKTITLE = {Proc.\ 3rd Workshop on Theory and Applications of
		 Abstract Data Types},
  LOCATION = {Bremen},
  PUBLISHER = {Springer},
  SERIES = {Informatik-Fachberichte},
  VOLUME = 116,
  PAGES = {31--38},
  YEAR = 1985,
  POSTSCRIPT = {http://homepages.inf.ed.ac.uk/dts/pub/thoughts.ps},
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/thoughts.pdf},
  COMMENT = {[Reviewed in Zbl 584.68036.]}
}

@ARTICLE{SannellaDT:completeness85,
  AUTHOR = {David MacQueen and Donald Sannella},
  TITLE = {Completeness of Proof Systems for Equational
		 Specifications},
  JOURNAL = {{IEEE} Trans.\ on Software Engineering},
  VOLUME = {{SE}-11},
  NUMBER = 5,
  PAGES = {454--461},
  YEAR = 1985,
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/completeness.pdf},
  ABSTRACT = {Contrary to popular belief, equational logic with induction is not
complete for initial models of equational specifications.  Indeed,
under some regimes (the Clear specification language and most other
algebraic specification languages) no proof system exists which is
complete even with respect to ground equations.  A collection of known
results is presented along with some new observations.},
  COMMENT = {[Reviewed in Zbl 558.68017.]}
}

@INPROCEEDINGS{SannellaDT:observational-equivalence85,
  AUTHOR = {Donald Sannella and Andrzej Tarlecki},
  TITLE = {On Observational Equivalence and Algebraic
		 Specification},
  YEAR = 1985,
  BOOKTITLE = {Proc.\ 10th Colloq.\ on Trees in Algebra and
		 Programming.  Intl.\ Joint Conf.\ on Theory and
		 Practice of Software Development ({TAPSOFT}'85)},
  LOCATION = {Berlin},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = 185,
  PUBLISHER = {Springer},
  PAGES = {308--322},
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/obs-equiv-conf.pdf},
  NOTE = {\textbf{Extended abstract; the final full version of this is
\cite{SannellaDT:observational-equivalence87}}},
  ABSTRACT = {The properties of a simple and natural notion of observational
equivalence of algebras and the corresponding specification-building
operation (observational abstraction) are studied. We begin with a
definition of observational equivalence which is adequate to handle
reachable algebras only, and show how to extend it to cope with
unreachable algebras and also how it may be generalised to make
sense under an arbitrary institution . Behavioural equivalence is
treated as an important special case of observational equivalence, and
its central role in program development is shown by means of an example.},
  COMMENT = {[Long version: Report CSR-172-84, Dept. of Computer
		 Science, Univ. of Edinburgh, 1984.]}
}

@ARTICLE{SannellaDT:observational-equivalence87,
  AUTHOR = {Donald Sannella and Andrzej Tarlecki},
  TITLE = {On Observational Equivalence and Algebraic
		 Specification},
  JOURNAL = {Journal of Computer and System Sciences},
  VOLUME = 34,
  PAGES = {150--178},
  YEAR = 1987,
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/obs-equiv.pdf},
  ABSTRACT = {The properties of a simple and natural notion of observational
equivalence of algebras and the corresponding specification-building
operation are studied.  We begin with a definition of observational
equivalence which is adequate to handle reachable algebras only, and
show how to extend it to cope with unreachable algebras and also how
it may be generalised to make sense under an arbitrary institution.
Behavioural equivalence is treated as an important special case of
observational equivalence, and its central role in program development
is shown by means of an example.},
  COMMENT = {[Reviewed in MR 88j:68118 and CR 8808-0615; this is
		 the final complete version of
		 \cite{SannellaDT:observational-equivalence85}.]}
}

@INPROCEEDINGS{SannellaDT:implementations-revisited87,
  AUTHOR = {Donald Sannella and Andrzej Tarlecki},
  TITLE = {Toward Formal Development of Programs from Algebraic
		 Specifications: Implementations Revisited},
  BOOKTITLE = {Proc.\ 12th Colloq.\ on Trees in Algebra and
		 Programming.  Intl.\ Joint Conf.\ on Theory and
		 Practice of Software Development ({TAPSOFT}'87)},
  LOCATION = {Pisa},
  PUBLISHER = {Springer},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = 249,
  PAGES = {96--110},
  YEAR = 1987,
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/impl-conf.pdf},
  ABSTRACT = {The program development process is viewed as a sequence of
implementation steps leading from a specification to a program. Based
on an elementary notion of refinement, two notions of implementation
are studied: constructor implementations which involve a construction
``on top of'' the implementing specification, and abstractor
implementations which additionally provide for abstraction from some
details of the implemented specification. These subsume most formal
notions of implementation in the literature. Both kinds of
implementations satisfy a vertical composition and a (modified)
horizontal composition property. All the definitions and results
generalise to the framework of an arbitrary institution.},
  NOTE = {\textbf{Extended abstract; the final full version of this is
 \cite{SannellaDT:implementations-revisited88}}}
}

@ARTICLE{SannellaDT:implementations-revisited88,
  AUTHOR = {Donald Sannella and Andrzej Tarlecki},
  TITLE = {Toward Formal Development of Programs from Algebraic
		 Specifications: Implementations Revisited},
  JOURNAL = {Acta Informatica},
  VOLUME = 25,
  PAGES = {233--281},
  YEAR = 1988,
  POSTSCRIPT = {http://homepages.inf.ed.ac.uk/dts/pub/impl.ps},
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/impl.pdf},
  ABSTRACT = {The program development process is viewed as a sequence of
implementation steps leading from a specification to a program.  Based
on an elementary notion of refinement, two notions of implementation
are studied: constructor implementations which involve a construction
``on top of'' the implementing specification, and abstractor
implementations which additionally provide for abstraction from some
details of the implemented specification.  These subsume most formal
notions of implementation in the literature.  Both kinds of
implementations satisfy a vertical composition and a (modified)
horizontal composition property.  All the definitions and results are
shown to generalise to the framework of an arbitrary institution, and
a way of changing institutions during the implementation process is
introduced.  All this is illustrated by means of simple concrete
examples.},
  COMMENT = {[This is the final version of
		 \cite{SannellaDT:implementations-revisited87}.]}
}

@ARTICLE{SannellaDT:lfcs-newsletter-survey88,
  AUTHOR = {Donald Sannella},
  TITLE = {Algebraic Specification and Formal Program
		 Development: Motivation, Present State and Future
		 Prospects},
  JOURNAL = {{LFCS} Newsletter},
  VOLUME = 1,
  PAGES = {7--10},
  YEAR = 1988
}

@ARTICLE{SannellaDT:lfcs-newsletter-tools88,
  AUTHOR = {Donald Sannella and Andrzej Tarlecki},
  TITLE = {Tools for Formal Program Development: Some
		 Fantasies},
  JOURNAL = {{LFCS} Newsletter},
  VOLUME = 1,
  PAGES = {10--15},
  YEAR = 1988
}

@INPROCEEDINGS{SannellaDT:structure-representation89,
  AUTHOR = {Robert Harper and Donald Sannella and
		 Andrzej Tarlecki},
  TITLE = {Structure and Representation in {LF}},
  BOOKTITLE = {Proc.\ 4th {IEEE} Symp.\ on Logic in Computer
		 Science},
  LOCATION = {Asilomar},
  PAGES = {226--237},
  YEAR = 1989,
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/lf-conf.pdf},
  NOTE = {\textbf{Extended abstract; the final full version of this is
\cite{SannellaDT:structured-presentations94}}},
  ABSTRACT = {The purpose of a logical framework such as LF is to provide a language for
defining logical systems suitable for use in a logic-independent proof
development environment.  All inferential activity in an object logic (in
particular, proof search) is to be conducted in the logical framework via the
representation of that logic in the framework.  An important tool for
controlling search in an object logic is the use of structured theory
presentations.  In order to apply these ideas to the setting of a logical
framework, we study the behavior of structured theory presentations under
representation in a framework, focusing on the problem of ``lifting''
presentations from the object logic to the metalogic of the framework.
We also consider imposing structure on logic presentations so that logical
systems may themselves be defined in a modular fashion.  This opens the way to
a CLEAR-like language for defining both theories and logics in a logical
framework.},
  COMMENT = {[This is an extended abstract of
		 \cite{SannellaDT:structure-representation89a}, which is a
		 preliminary version of
		 \cite{SannellaDT:structured-presentations94}.]}
}

@INPROCEEDINGS{SannellaDT:structure-representation89a,
  AUTHOR = {Robert Harper and Donald Sannella and
		 Andrzej Tarlecki},
  TITLE = {Structure and Representation in {LF}},
  BOOKTITLE = {Proc.\ 1989 Workshop on Programming Logic},
  LOCATION = {B\aa{}stad},
  PAGES = {232--257},
  YEAR = 1989,
  NOTE = {\textbf{Extended abstract; the final full version of this is
\cite{SannellaDT:structured-presentations94}}},
  COMMENT = {[This is a longer version of
		 \cite{SannellaDT:structure-representation89} and a
		 preliminary version of
		 \cite{SannellaDT:structured-presentations94}.]}
}

@ARTICLE{SannellaDT:structured-presentations94,
  AUTHOR = {Robert Harper and Donald Sannella and
		 Andrzej Tarlecki},
  TITLE = {Structured Presentations and Logic Representations},
  JOURNAL = {Annals of Pure and Applied Logic},
  VOLUME = 67,
  PAGES = {113--160},
  YEAR = 1994,
  POSTSCRIPT = {http://homepages.inf.ed.ac.uk/dts/pub/apal.ps},
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/apal.pdf},
  ABSTRACT = {The purpose of a logical framework such as LF is to provide a
language for defining logical systems suitable for use in a
logic-independent proof development environment.  All inferential
activity in an object logic (in particular, proof search) is to be
conducted in the logical framework via the representation of that
logic in the framework.  An important tool for controlling search in
an object logic, the need for which is motivated by the difficulty of
reasoning about large and complex systems, is the use of structured
theory presentations.  In this paper a rudimentary language of
structured theory presentations is presented, and the use of this
structure in proof search for an arbitrary object logic is explored.
The behaviour of structured theory presentations under representation
in a logical framework is studied, focusing on the problem of
``lifting'' presentations from the object logic to the metalogic of
the framework.  The topic of imposing structure on logic
presentations, so that logical systems may themselves be defined in a
modular fashion, is also briefly considered.},
  COMMENT = {[Reviewed in MR~95i:03024;
		 this is the extended final version of
		 \cite{SannellaDT:structure-representation89} and
		 \cite{SannellaDT:structure-representation89a}.]}
}

@INPROCEEDINGS{SannellaDT:logic-representation89,
  AUTHOR = {Robert Harper and Donald Sannella and
		 Andrzej Tarlecki},
  TITLE = {Logic Representation in {LF}},
  VOLUME = 389,
  SERIES = {Lecture Notes in Computer Science},
  PAGES = {250--272},
  BOOKTITLE = {Proc.\ 3rd Summer Conf.\ on Category Theory and
		 Computer Science},
  LOCATION = {Manchester},
  YEAR = 1989,
  PUBLISHER = {Springer},
  ABSTRACT = {The purpose of a logical framework such as LF is to provide a
language for defining logical systems suitable for use in a
logic-independent proof development environment.  In previous work we
have developed a theory of representation of logics in a logical
framework and considered the behaviour of structured theory
presentations under representation.  That work was based on the
simplifying assumption that logics are characterized as families of
consequence relations on ``closed'' sentences.  In this report we
extend the notion of logical system to account for open formula, and
study its basic properties.  Following standard practice, we
distinguish two types of logical system of open formulae that differ
in the treatment of free variables, and show how they may be induced
from a logical system of closed sentences.  The technical notions of a
logic presentation and a uniform encoding of a logical system in LF
are generalized to the present setting.}
}

@INCOLLECTION{SannellaDT:real-problems93,
  AUTHOR = {Donald Sannella and Andrzej Tarlecki},
  TITLE = {Algebraic Specification and Formal Methods for
		 Program Development: What are the Real Problems?},
  BOOKTITLE = {Current Trends in Theoretical Computer Science.
		 Essays and Tutorials},
  PUBLISHER = {World Scientific},
  EDITOR = {G. Rozenberg and A. Salomaa},
  PAGES = {115--120},
  YEAR = 1993,
  POSTSCRIPT = {http://homepages.inf.ed.ac.uk/dts/pub/problems.ps},
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/problems.pdf},
  ABSTRACT = {The long-term goal of work on algebraic specification is formal
development of correct programs from specifications via
verified-correct refinement steps.  Define a \emph{real problem} to
be an unsolved problem which lies on (or near) the path betwen the
current state of the art and this ultimate goal.  Long-term progress
depends on solving these problems, so it seems worthwhile to attack
the real problems before worrying about other issues.

It is perhaps surprising that there is little agreement concerning
what these problems are, at least if one takes the problems being
tackled as an indication of what various researchers think the real
problems are.  Some sort of consensus seems desirable to promote
effective joint progress towards our common goal.

We list some (not all) of what we think are the real problems.  In an
attempt to spark controversy, some things which we think are not real
problems are also listed.  Neither of these lists is exhaustive.},
  NOTE = {Originally published in \emph{EATCS Bulletin}
		 41:134--137 (1990).}
}

@BOOK{SannellaDT:compass-bibliography91,
  EDITOR = {Michel Bidoit and Hans-J{\"o}rg Kreowski and
		 Pierre Lescanne and Fernando Orejas and
		 Donald Sannella},
  TITLE = {Algebraic System Specification and Development:
		 A Survey and Annotated Bibliography},
  PUBLISHER = {Springer},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = 501,
  YEAR = 1991,
  COMMENT = {[Reviewed in CR 9209-0662.]}
}

@INPROCEEDINGS{SannellaDT:asl+91,
  AUTHOR = {Donald Sannella and Andrzej Tarlecki},
  TITLE = {A Kernel Specification Formalism with Higher-Order
		 Parameterisation},
  BOOKTITLE = {Proc.\ 7th Workshop on Specification of Abstract
		 Data Types},
  LOCATION = {Wusterhausen},
  PUBLISHER = {Springer},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = 534,
  PAGES = {274--296},
  YEAR = 1991,
  POSTSCRIPT = {http://homepages.inf.ed.ac.uk/dts/pub/spec-formalism.ps},
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/spec-formalism.pdf},
  ABSTRACT = {A specification formalism with parameterisation of an arbitrary order
is presented.  It is given a denotational-style semantics, accompanied
by an inference system for proving that an object satisfies a
specification.  The inference system incorporates, but is not limited
to, a clearly identified type-checking component.

Special effort is made to carefully distinguish between parameterised
specifications, which denote functions yielding classes of objects,
and specifications of parameterised objects, which denote classes of
functions yielding objects.  To deal with both of these in a uniform
framework, it was convenient to view specifications, which specify
objects, as objects themselves, and to introduce a notion of a
specification of specifications.

The formalism includes the basic specification-building operations of
the ASL specification language.  This choice, however, is orthogonal
to the new ideas presented.  The formalism is also
institution-independent, although this issue is not explicitly
discussed at any length here.},
  COMMENT = {[Superceded by Section 7 of
		 \cite{SannellaDT:parameterisation-revisited92}.]}
}

@ARTICLE{SannellaDT:parameterisation-revisited92,
  AUTHOR = {Donald Sannella and Stefan Soko{\l}owski and
		 Andrzej Tarlecki},
  TITLE = {Toward Formal Development of Programs from Algebraic
		 Specifications: Parameterisation Revisited},
  JOURNAL = {Acta Informatica},
  VOLUME = 29,
  NUMBER = 8,
  PAGES = {689--736},
  COMMENT = {[Reviewed in CR 9405-0310, CR 9503-0176; an early
		 version of this, with an extended example in an
		 appendix, appeared as report 6/90, Univ. Bremen,
		 1990.]},
  YEAR = 1992,
  POSTSCRIPT = {http://homepages.inf.ed.ac.uk/dts/pub/param.ps},
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/param.pdf},
  ABSTRACT = {Parameterisation is an important mechanism for structuring programs
and specifications into modular units.  The interplay between
parameterisation (of programs and of specifications) and specification
(of parameterised and of non-parameterised programs) is analysed,
exposing important semantic and methodological differences between
specifications of parameterised programs and parameterised
specifications.  The extension of parameterisation mechanisms to the
higher-order case is considered, both for parameterised programs and
parameterised specifications, and the methodological consequences of
such an extension are explored.

A specification formalism with parameterisation of an arbitrary order
is presented.  Its denotational-style semantics is accompanied by an
inference system for proving that an object satisfies a specification.
The formalism includes the basic specification-building operations of
the ASL specification language and is institution independent.}
}

@INPROCEEDINGS{SannellaDT:model-theoretic-foundations92,
  AUTHOR = {Donald Sannella and Andrzej Tarlecki},
  TITLE = {Toward Formal Development of Programs from Algebraic
		 Specifications: Model-Theoretic Foundations},
  BOOKTITLE = {Proc.\ 19th Intl.\ Colloq.\ on Automata,
		 Languages and Programming},
  LOCATION = {Vienna},
  PUBLISHER = {Springer},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = 623,
  PAGES = {656--671},
  YEAR = 1992,
  POSTSCRIPT = {http://homepages.inf.ed.ac.uk/dts/pub/mtf.ps},
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/mtf.pdf},
  ABSTRACT = {This paper presents in an informal way the main ideas underlying our work on
the model-theoretic foundations of algebraic specification and program
development.
We attempt to offer an overall view, rather than new results,
and focus on the basic motivation behind the technicalities
presented elsewhere and on the conclusions from this work.},
  NOTE = {\textbf{This is superceded by \cite{SannellaDT:essential-concepts97}}}
}

@ARTICLE{SannellaDT:essential-concepts97,
  AUTHOR = {Donald Sannella and Andrzej Tarlecki},
  TITLE = {Essential Concepts of Algebraic
		 Specification and Program Development},
  JOURNAL = {Formal Aspects of Computing},
  VOLUME = 9,
  PAGES = {229--269},
  YEAR = 1997,
  DVI = {http://homepages.inf.ed.ac.uk/dts/pub/concepts.dvi},
  POSTSCRIPT = {http://homepages.inf.ed.ac.uk/dts/pub/concepts.ps},
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/concepts.pdf},
  COMMENT = {[An early short version of this is \cite{SannellaDT:model-theoretic-foundations92}.]},
  ABSTRACT = {The main ideas underlying work on the model-theoretic foundations of
algebraic specification and formal program development are presented
in an informal way.  An attempt is made to offer an overall view,
rather than new results, and to focus on the basic motivation behind
the technicalities presented elsewhere.}
}

@INPROCEEDINGS{SannellaDT:behavioural-abstraction-hol95,
  AUTHOR = {Martin Hofmann and Donald Sannella},
  TITLE = {On Behavioural Abstraction and Behavioural
		 Satisfaction in Higher-Order Logic},
  BOOKTITLE = {Proc.\ 20th Colloq.\ on Trees in Algebra and
		 Programming.  Intl.\ Joint Conf.\ on Theory and
		 Practice of Software Development ({TAPSOFT}'95)},
  LOCATION = {Aarhus},
  PUBLISHER = {Springer},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = 915,
  PAGES = {247--261},
  YEAR = 1995,
  NOTE = {\textbf{The final full version of this is \cite{SannellaDT:behavioural-abstraction-hol96}}},
  DVI = {http://homepages.inf.ed.ac.uk/dts/pub/beh-equiv.dvi},
  POSTSCRIPT = {http://homepages.inf.ed.ac.uk/dts/pub/beh-equiv.ps},
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/beh-equiv.pdf},
  ABSTRACT = {The behavioural semantics of specifications with higher-order logical
formulae as axioms is analyzed.  A characterization of behavioural
abstraction via behavioural satisfaction of formulae in which the
equality symbol is interpreted as indistinguishability, which is due
to Reichel and was recently generalized to the case of first-order
logic by Bidoit \emph{et al}, is further generalized to this case.  The
fact that higher-order logic is powerful enough to express the
indistinguishability relation is used to characterize behavioural
satisfaction in terms of ordinary satisfaction, and to develop new
methods for reasoning about specifications under behavioural
semantics.}
}

@ARTICLE{SannellaDT:behavioural-abstraction-hol96,
  AUTHOR = {Martin Hofmann and Donald Sannella},
  TITLE = {On Behavioural Abstraction and Behavioural
		 Satisfaction in Higher-Order Logic},
  JOURNAL = {Theoretical Computer Science},
  VOLUME = 167,
  PAGES = {3--45},
  YEAR = 1996,
  DVI = {http://homepages.inf.ed.ac.uk/dts/pub/beh-equiv-tcs.dvi},
  POSTSCRIPT = {http://homepages.inf.ed.ac.uk/dts/pub/beh-equiv-tcs.ps},
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/beh-equiv-tcs.pdf},
  ABSTRACT = {The behavioural semantics of specifications with higher-order logical
formulae as axioms is analyzed.  A characterization of behavioural
abstraction via behavioural satisfaction of formulae in which the
equality symbol is interpreted as indistinguishability, which is due
to Reichel and was recently generalized to the case of first-order
logic by Bidoit \emph{et al}, is further generalized to this case.  The
fact that higher-order logic is powerful enough to express the
indistinguishability relation is used to characterize behavioural
satisfaction in terms of ordinary satisfaction, and to develop new
methods for reasoning about specifications under behavioural
semantics.},
  COMMENT = {[This is the full version of
		 \cite{SannellaDT:behavioural-abstraction-hol95}.]}
}

@INCOLLECTION{SannellaDT:prelimaries96,
  AUTHOR = {Donald Sannella and Andrzej Tarlecki},
  TITLE = {Algebraic Preliminaries},
  BOOKTITLE = {Algebraic Foundations of Systems Specification},
  PUBLISHER = {Springer},
  CHAPTER = 2,
  EDITOR = {Egidio Astesiano and Hans-J{\"o}rg Kreowski and
		 Bernd Krieg-Br{\"u}ckner},
  YEAR = 1999,
  DVI = {http://homepages.inf.ed.ac.uk/dts/pub/prelim.dvi},
  POSTSCRIPT = {http://homepages.inf.ed.ac.uk/dts/pub/prelim.ps},
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/prelim.pdf}
}

@INCOLLECTION{SannellaDT:specification-languages96,
  AUTHOR = {Donald Sannella and Martin Wirsing},
  TITLE = {Specification Languages},
  BOOKTITLE = {Algebraic Foundations of Systems Specification},
  PUBLISHER = {Springer},
  CHAPTER = 8,
  EDITOR = {Egidio Astesiano and Hans-J{\"o}rg Kreowski and
		 Bernd Krieg-Br{\"u}ckner},
  YEAR = 1999,
  DVI = {http://homepages.inf.ed.ac.uk/dts/pub/spec-lang.dvi},
  POSTSCRIPT = {http://homepages.inf.ed.ac.uk/dts/pub/spec-lang.ps},
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/spec-lang.pdf}
}

@INPROCEEDINGS{SannellaDT:mind-the-gap96,
  AUTHOR = {Donald Sannella and Andrzej Tarlecki},
  TITLE = {Mind the Gap! {A}bstract versus Concrete Models of
		 Specifications},
  BOOKTITLE = {Proc.\ 21st Intl.\ Symp.\ on Mathematical
		 Foundations of Computer Science},
  LOCATION = {Cracow},
  PUBLISHER = {Springer},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = 1113,
  PAGES = {114--134},
  YEAR = 1996,
  DVI = {http://homepages.inf.ed.ac.uk/dts/pub/mfcs96.dvi},
  POSTSCRIPT = {http://homepages.inf.ed.ac.uk/dts/pub/mfcs96.ps},
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/mfcs96.pdf},
  ABSTRACT = {In the theory of algebraic specifications, many-sorted algebras are
used to model programs: the representation of data is arbitrary and
operations are modelled as ordinary functions.  The theory that
underlies the formal development of programs from specifications takes
advantage of the many useful properties that these models enjoy.

The models that underlie the semantics of programming languages are
different.  For example, the semantics of Standard~ML uses rather
concrete models, where data values are represented as closed
constructor terms and functions are represented as ``closures''.  The
properties of these models are quite different from those of
many-sorted algebras.

This discrepancy brings into question the applicability of the theory
of specification and formal program development in the context of a
concrete programming language, as has been attempted in the
Extended~ML framework for the formal development of Standard~ML
programs.  This paper is a preliminary study of the difference between
abstract and concrete models of specifications, inspired by the kind
of concrete models used in the semantics of Standard~ML, in an attempt
to determine the consequences of the discrepancy.}
}

@ARTICLE{SannellaDT:alg-methods99,
  AUTHOR = {Donald Sannella and
		 Andrzej Tarlecki},
  TITLE = {Algebraic Methods for Specification and Formal
		Development of Programs},
  JOURNAL = {ACM Computing Surveys},
  VOLUME = 31,
  NUMBER = {3es},
  YEAR = 1999,
  DVI = {http://homepages.inf.ed.ac.uk/dts/pub/computing-surveys.dvi},
  POSTSCRIPT = {http://homepages.inf.ed.ac.uk/dts/pub/computing-surveys.ps},
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/computing-surveys.pdf},
  ABSTRACT = {This note gives our personal perspective on the state of foundations of software
specification and development including applications to the formal development of
reliable complex software systems.}
}

@INPROCEEDINGS{SannellaDT:lax-logical-relations00,
  AUTHOR = {Gordon Plotkin and John Power and Donald Sannella and Robert Tennent},
  TITLE = {Lax Logical Relations},
  BOOKTITLE = {Proc.\ 27th Intl.\ Colloq.\ on Automata, Languages
	and Programming},
  LOCATION = {Geneva},
  PUBLISHER = {Springer},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = 1853,
  PAGES = {85--102},
  YEAR = 2000,
  DVI = {http://homepages.inf.ed.ac.uk/dts/pub/laxlogrel.dvi},
  POSTSCRIPT = {http://homepages.inf.ed.ac.uk/dts/pub/laxlogrel.ps},
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/laxlogrel.pdf},
  ABSTRACT = {Lax logical relations are a categorical generalisation of logical
relations; though they preserve product types, they need not preserve
exponential types.  But, like logical relations, they are preserved by
the meanings of all lambda-calculus terms.  We show that lax logical
relations coincide with the correspondences of Schoett, the algebraic
relations of Mitchell and the pre-logical relations of Honsell and
Sannella on Henkin models, but also generalise naturally to models in
cartesian closed categories and to richer languages.}
}

@INPROCEEDINGS{SannellaDT:prelogical-relations99,
  AUTHOR = {Furio Honsell and Donald Sannella},
  TITLE = {Pre-logical Relations},
  BOOKTITLE = {Proc.\ Computer Science Logic, CSL'99},
  LOCATION = {Madrid},
  PUBLISHER = {Springer},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = 1683,
  PAGES = {546--561},
  YEAR = 1999,
  DVI = {http://homepages.inf.ed.ac.uk/dts/pub/prelogrel.dvi},
  POSTSCRIPT = {http://homepages.inf.ed.ac.uk/dts/pub/prelogrel.ps},
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/prelogrel.pdf},
  ABSTRACT = {We study a weakening of the notion of logical relations, called
pre-logical relations, that has many of the features that make logical
relations so useful as well as further algebraic properties including
composability.  The basic idea is simply to require the reverse
implication in the definition of logical relations to hold only for
pairs of functions that are expressible by the same lambda term.
Pre-logical relations are the minimal weakening of logical relations
that gives composability for extensional structures and simultaneously
the most liberal definition that gives the Basic Lemma.  The use of
pre-logical relations in place of logical relations gives an improved
version of Mitchell's representation independence theorem which
characterizes observational equivalence for all signatures rather than
just for first-order signatures.  Pre-logical relations can be used in
place of logical relations to give an account of data refinement where
the fact that pre-logical relations compose explains why stepwise
refinement is sound.},
  NOTE = {\textbf{The final full version of this is \cite{SannellaDT:prelogical-relations00}}}
}

@ARTICLE{SannellaDT:prelogical-relations00,
  AUTHOR = {Furio Honsell and Donald Sannella},
  TITLE = {Prelogical Relations},
  JOURNAL = {Information and Computation},
  YEAR = {2002},
  VOLUME = {178},
  PAGES = {23--43},
  DVI = {http://homepages.inf.ed.ac.uk/dts/pub/prelogrel-long.dvi},
  POSTSCRIPT = {http://homepages.inf.ed.ac.uk/dts/pub/prelogrel-long.ps},
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/prelogrel-long.pdf},
  ABSTRACT = {We study a weakening of the notion of logical relations, called
prelogical relations, that has many of the features that make logical
relations so useful as well as further algebraic properties including
composability.  The basic idea is simply to require the reverse
implication in the definition of logical relations to hold only for
pairs of functions that are expressible by the same lambda term.
Prelogical relations are the minimal weakening of logical relations
that gives composability for extensional structures and simultaneously
the most liberal definition that gives the Basic Lemma.  Prelogical predicates (i.e., unary prelogical relations) coincide
with sets that are invariant under Kripke logical relations with
varying arity as introduced by Jung and Tiuryn, and prelogical
relations are the closure under projection and intersection of logical
relations.
These conceptually independent characterizations of prelogical
relations suggest that the concept is rather intrinsic and robust.
The use of
prelogical relations gives an improved
version of Mitchell's representation independence theorem which
characterizes observational equivalence for all signatures rather than
just for first-order signatures.  Prelogical relations can be used in
place of logical relations to give an account of data refinement where
the fact that prelogical relations compose explains why stepwise
refinement is sound.},
  COMMENT = {[This is an
extended version of \cite{SannellaDT:prelogical-relations99} that supercedes
Report ECS-LFCS-99-405, Laboratory for Foundations of Computer Science,
Univ.\ of Edinburgh (1999).]}
}

@INPROCEEDINGS{SannellaDT:refinement99,
  AUTHOR = {Donald Sannella},
  TITLE = {Algebraic Specification and Program Development
	by Stepwise Refinement},
  BOOKTITLE = {Proc.\ 9th Intl.\ Workshop on
	Logic-based Program Synthesis and Transformation, {LOPSTR}'99},
  LOCATION = {Venice},
  PUBLISHER = {Springer},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = 1817,
  PAGES = {1--9},
  YEAR = 2000,
  DVI = {http://homepages.inf.ed.ac.uk/dts/pub/lopstr99.dvi},
  POSTSCRIPT = {http://homepages.inf.ed.ac.uk/dts/pub/lopstr99.ps},
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/lopstr99.pdf},
  ABSTRACT = {Various formalizations of the concept of ``refinement step'' as used
in the formal development of programs from algebraic specifications
are presented and compared.}
}

@INPROCEEDINGS{SannellaDT:constructive-refinement00,
  AUTHOR = {Furio Honsell and John Longley and Donald Sannella and Andrzej Tarlecki},
  TITLE = {Constructive Data Refinement in Typed Lambda Calculus},
  BOOKTITLE = {Proc.\ 3rd Intl.\ Conf.\ on Foundations of Software
		Science and Computation Structures.
		European Joint Conferences on Theory and Practice of
		Software ({ETAPS} 2000)},
  LOCATION = {Berlin},
  PUBLISHER = {Springer},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = 1784,
  PAGES = {161--176},
  YEAR = 2000,
  POSTSCRIPT = {http://homepages.inf.ed.ac.uk/dts/pub/refinement.ps},
  DVI = {http://homepages.inf.ed.ac.uk/dts/pub/refinement.dvi},
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/refinement.pdf},
  ABSTRACT = {A new treatment of data refinement in typed lambda calculus is proposed,
phrased in terms of pre-logical relations [HS99] rather than logical
relations, and incorporating a constructive element.  Constructive data
refinement is shown to have desirable properties, and a substantial example
of refinement is presented.}
}

@INPROCEEDINGS{SannellaDT:simulation-relations03,
  AUTHOR = {Jo Hannay and {Shin-ya} Katsumata and Donald Sannella},
  TITLE = {Semantic and Syntactic Approaches to Simulation Relations},
  BOOKTITLE = {Proc.\ 28th Intl.\ Symp.\ on Mathematical
		 Foundations of Computer Science},
  LOCATION = {Bratislava},
  PUBLISHER = {Springer},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = 2747,
  PAGES = {68--91},
  YEAR = 2003,
  DVI = {http://homepages.inf.ed.ac.uk/dts/pub/mfcs2003.dvi},
  POSTSCRIPT = {http://homepages.inf.ed.ac.uk/dts/pub/mfcs2003.ps},
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/mfcs2003.pdf},
  ABSTRACT = {Simulation relations are tools for establishing the correctness of
data refinement steps.  In the simply-typed lambda calculus, logical
relations are the standard choice for simulation relations, but they
suffer from certain shortcomings; these are resolved by use of the
weaker notion of pre-logical relations instead.  Developed from a
syntactic setting, abstraction barrier-observing simulation
relations serve the same purpose, and also handle polymorphic
operations.  Meanwhile, second-order pre-logical relations directly
generalise pre-logical relations to polymorphic lambda calculus
(System F).  We compile the main refinement-pertinent results of
these various notions of simulation relation, and try to raise some
issues for aiding their comparison and reconciliation.}
}

@INPROCEEDINGS{SannellaDT:global-dev02,
  AUTHOR = {Michel Bidoit and Donald Sannella and Andrzej Tarlecki},
  TITLE = {Global Development via Local Observational Construction Steps},
  BOOKTITLE = {Proc.\ 27th Intl.\ Symp.\ on Mathematical
		 Foundations of Computer Science},
  LOCATION = {Warsaw},
  PUBLISHER = {Springer},
  SERIES = {Lecture Notes in Computer Science},
  YEAR = 2002,
  VOLUME = 2420,
  PAGES = {1--24},
  DVI = {http://homepages.inf.ed.ac.uk/dts/pub/global-dev.dvi},
  POSTSCRIPT = {http://homepages.inf.ed.ac.uk/dts/pub/global-dev.ps},
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/global-dev.pdf},
  NOTE = {\textbf{An extended version appeared in \cite{SannellaDT:obs-interp-casl-specs08}}},
  ABSTRACT = {The way that refinement of individual ``local'' components of a
specification relates to development of a ``global'' system from a
specification of requirements is explored.  Observational
interpretation of specifications and refinements add expressive power
and flexibility while bringing in some subtle problems.
The results are instantiated in the context of CASL architectural
specifications.}
}

@INPROCEEDINGS{SannellaDT:horizontal-composition06,
  AUTHOR = {Donald Sannella and Andrzej Tarlecki},
  TITLE = {Horizontal Composability Revisited},
  BOOKTITLE = {Algebra, Meaning and Computation: Essays Dedicated to
Joseph A. Goguen on the Occasion of his 65th Birthday},
  PUBLISHER = {Springer},
  SERIES = {Lecture Notes in Computer Science},
  YEAR = 2006,
  VOLUME = 4060,
  PAGES = {296--316},
  POSTSCRIPT = {http://homepages.inf.ed.ac.uk/dts/pub/goguen-festschrift.ps},
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/goguen-festschrift.pdf},
  ABSTRACT = {We recall the contribution of Goguen and Burstall's 1980 CAT paper
and its powerful influence on theories of specification
implementation that were emerging at about the same time, via the
introduction of the notions of vertical and horizontal
composition of implementations.  We then give a different view of
implementation which we believe provides a more adequate reflection of
the rather subtle interplay between implementation, specification
structure and program structure.}
}

@INPROCEEDINGS{SannellaDT:observability08,
  AUTHOR = {Donald Sannella and Andrzej Tarlecki},
  TITLE = {Observability Concepts in Abstract Data Type Specification,
30 Years Later},
  BOOKTITLE = {Concurrency, Graphs and Models: Essays Dedicated to
Ugo Montanari on the Occasion of his 65th Birthday},
  PUBLISHER = {Springer},
  SERIES = {Lecture Notes in Computer Science},
  YEAR = 2008,
  POSTSCRIPT = {http://homepages.inf.ed.ac.uk/dts/pub/montanari-festschrift.ps},
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/montanari-festschrift.pdf},
  ABSTRACT = {We recall the contribution of Montanari's paper [GGM76] and
sketch a framework for observable behaviour specification that blends
some of these early ideas, seen from a more modern perspective, with
our own approach.}
}

@INPROCEEDINGS{SannellaDT:eml-intro85,
  AUTHOR = {Donald Sannella and Andrzej Tarlecki},
  TITLE = {Program Specification and Development in
		 {S}tandard {ML}},
  BOOKTITLE = {Proc.\ 12th {ACM} Symp.\ on Principles of
		 Programming Languages},
  LOCATION = {New Orleans},
  PAGES = {67--77},
  YEAR = 1985,
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/eml-popl.pdf},
  ABSTRACT = {An attempt is made to apply ideas about algebraic specification in
the context of a programming language.  Standard ML with modules is
extended by allowing axioms in module interface specifications and in
place of code.  The resulting specification language, called Extended
ML, is given a semantics based on the primitive specification-building
operations of the kernel algebraic specification language
ASL. Extended ML provides a framework for the formal development of
programs from specifications by stepwise refinement, which is
illustrated by means of a simple example.  From its semantic basis
Extended ML inherits complete independence from the logical system
(institution) used to write specifications.  This allows different
styles of specification as well as different programming languages to
be accommodated.},
  COMMENT = {[Obsolete with respect to the current design of
		 Extended ML.]}
}

@INPROCEEDINGS{SannellaDT:eml-institution-independent86,
  AUTHOR = {Donald Sannella and Andrzej Tarlecki},
  TITLE = {Extended {ML}: An Institution-Independent Framework
		 for Formal Program Development},
  BOOKTITLE = {Proc.\ Workshop on Category Theory and Computer
		 Programming},
  LOCATION = {Guildford},
  PUBLISHER = {Springer},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = 240,
  PAGES = {364--389},
  YEAR = 1986,
  POSTSCRIPT = {http://homepages.inf.ed.ac.uk/dts/pub/abstract-eml.ps},
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/abstract-eml.pdf},
  ABSTRACT = {The Extended ML specification language provides a framework for the
formal stepwise development of modular programs in the Standard ML
programming language from specifications.  The object of this paper is
to equip Extended ML with a semantics which is completely independent
of the logical system used to write specifications, building on Goguen
and Burstall's work on the notion of an \emph{institution} as a
formalisation of the concept of a logical system.  One advantage of
this is that it permits freedom in the choice of the logic used in
writing specifications; an intriguing side-effect is that it enables
Extended ML to be used to develop programs in languages other than
Standard ML since we view programs as simply Extended ML
specifications which happen to include only ``executable'' axioms.
The semantics of Extended ML is defined in terms of the primitive
specification-building operations of the ASL kernel specification
language which itself has an institution-independent semantics.

It is not possible to give a semantics for Extended ML in an
institutional framework without extending the notion of an
institution; the new notion of an \emph{institution with syntax} is
introduced to provide an adequate foundation for this enterprise.  An
institution with syntax is an institution with three additions: the
category of signatures is assumed to form a concrete category; an
additional functor is provided which gives concrete syntactic
representations of sentences; and a natural transformation associates
these concrete objects with the ``abstract'' sentences they represent.
We use the first addition to ``lift'' certain necessary set-theoretic
constructions to the category of signatures, and the other two
additions to deal with the low-level semantics of axioms.},
  COMMENT = {[Reviewed in MR~88f:68100; somewhat obsolete with
		 respect to the current design of Extended ML but
		 the technicalities are still relevant.]}
}

@INPROCEEDINGS{SannellaDT:eml-tutorial87,
  AUTHOR = {Donald Sannella},
  TITLE = {Formal Specification of {ML} Programs},
  BOOKTITLE = {Jornadas Rank Xerox Sobre Inteligencia Artificial
		 Razonamiento Automatizado},
  LOCATION = {Blanes},
  PAGES = {79--98},
  YEAR = 1987,
  POSTSCRIPT = {http://homepages.inf.ed.ac.uk/dts/pub/ml-spec.ps},
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/ml-spec.pdf},
  ABSTRACT = {A tutorial introduction to specifying ML programs using ideas from
Extended ML}
}

@INPROCEEDINGS{SannellaDT:eml-methodology89,
  AUTHOR = {Donald Sannella and Andrzej Tarlecki},
  TITLE = {Toward Formal Development of {ML} Programs:
		 Foundations and Methodology},
  BOOKTITLE = {Proc.\ Colloq.\ on Current Issues in Programming
		 Languages.  Intl.\ Joint Conf.\ on Theory and
		 Practice of Software Development ({TAPSOFT}'89)},
  LOCATION = {Barcelona},
  PUBLISHER = {Springer},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = 352,
  PAGES = {375--389},
  YEAR = 1989,
  POSTSCRIPT = {http://homepages.inf.ed.ac.uk/dts/pub/eml-methodology.ps},
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/eml-methodology.pdf},
  ABSTRACT = {A formal methodology is presented for the systematic evolution of
modular Standard ML programs from specifications by means of verified
refinement steps, in the framework of the Extended ML specification
language. Program development proceeds via a sequence of
\emph{design} (modular decomposition) \emph{coding} and
\emph{refinement} steps.  For each of these three kinds of steps,
conditions are given which ensure the correctness of the result.
These conditions seem to be as weak as possible under the constraint
of being expressible as ``local'' interface matching requirements.
Interfaces are only required to match up to behavioural equivalence,
which is seen as vital to the use of data abstraction in program
development.},
  COMMENT = {[Long version: Report ECS-LFCS-89-71, Dept. of
		 Computer Science, Univ. of Edinburgh, 1989.]}
}

@INPROCEEDINGS{SannellaDT:eml-working-programmer91,
  AUTHOR = {Donald Sannella},
  TITLE = {Formal Program Development in {E}xtended {ML} for the
		 Working Programmer},
  BOOKTITLE = {Proc.\ 3rd {BCS}/{FACS} Workshop on Refinement},
  LOCATION = {Hursley Park},
  PUBLISHER = {Springer},
  SERIES = {Workshops in Computing},
  PAGES = {99--130},
  YEAR = 1991,
  POSTSCRIPT = {http://homepages.inf.ed.ac.uk/dts/pub/bcs.ps},
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/bcs.pdf},
  ABSTRACT = {Extended ML is a framework for the formal development of programs in
the Standard ML programming language from high-level specifications of
their required input/output behaviour.  It strongly supports the
development of modular programs consisting of an interconnected
collection of generic and reusable units.  The Extended ML framework
includes a methodology for formal program development which
establishes a number of ways of proceeding from a given specification
of a programming task towards a program.  Each such step gives rise to
one or more proof obligations which must be proved in order to
establish the correctness of that step.  This paper is intended as a
user-oriented summary of the Extended ML language and methodology.
Theoretical technicalities are avoided whenever possible, with
emphasis placed on the practical aspects of formal program
development.  An extended example of a complete program development in
Extended ML is included.}
}

@INPROCEEDINGS{SannellaDT:eml-overview91,
  AUTHOR = {Donald Sannella and Andrzej Tarlecki},
  TITLE = {{E}xtended {ML}: Past, Present and Future},
  BOOKTITLE = {Proc.\ 7th Workshop on Specification of Abstract
		 Data Types},
  LOCATION = {Wusterhausen},
  PUBLISHER = {Springer},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = 534,
  PAGES = {297--322},
  YEAR = 1991,
  POSTSCRIPT = {http://homepages.inf.ed.ac.uk/dts/pub/eml-overview.ps},
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/eml-overview.pdf},
  ABSTRACT = {An overview of past, present and future work on the Extended ML
formal program development framework is given, with emphasis on two
topics of current active research: the semantics of the Extended ML
specification language, and tools to support formal program
development.}
}

@INPROCEEDINGS{SannellaDT:spectral91,
  AUTHOR = {Bernd Krieg-Br{\"u}ckner and Donald Sannella},
  TITLE = {Structuring Specifications in-the-Large and
		 in-the-Small: Higher-Order Functions, Dependent Types
		 and Inheritance in {SPECTRAL}},
  BOOKTITLE = {Proc.\ Colloq.\ on Combining Paradigms for
		 Software Development.  Intl.\ Joint Conf.\ on Theory
		 and Practice of Software Development ({TAPSOFT}'91)},
  LOCATION = {Brighton},
  PUBLISHER = {Springer},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = 494,
  PAGES = {103--120},
  YEAR = 1991,
  POSTSCRIPT = {http://homepages.inf.ed.ac.uk/dts/pub/spectral.ps},
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/spectral.pdf},
  ABSTRACT = {SPECTRAL is an experiment in specification language design that tries
to maintain compactness in spite of a number of orthogonal concepts.
The design is based on Extended ML and PROSPECTRA, generalising and
extending both approaches.  Of particular concern are the means for
structuring specifications and programs in-the-large and in-the-small.
The language includes constructs for defining general higher-order
functions yielding specifications or program modules.  Concepts of
subtyping and (object-oriented) inheritance are included to support
the specification development process and to enhance re-usability.
Much of the power of the language comes from the use of dependent
types.}
}

@INPROCEEDINGS{SannellaDT:eml-gentle-intro93,
  AUTHOR = {Stefan Kahrs and Donald Sannella and
		 Andrzej Tarlecki},
  TITLE = {The Semantics of {E}xtended {ML}: A Gentle
		 Introduction},
  BOOKTITLE = {Proc.\ Intl.\ Workshop on Semantics of
		 Specification Languages},
  LOCATION = {Utrecht},
  PUBLISHER = {Springer},
  SERIES = {Workshops in Computing},
  PAGES = {186--215},
  YEAR = 1994,
  POSTSCRIPT = {http://homepages.inf.ed.ac.uk/dts/pub/gentle-conf.ps},
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/gentle-conf.pdf},
  ABSTRACT = {Extended ML (EML) is a framework for the formal development of
modular Standard ML (SML) software systems.  Development commences
with a specification of the behaviour required and proceeds via a
sequence of partial solutions until a complete solution, an executable
SML program, is obtained.  All stages in this development process are
expressed in the EML language, an extension of SML with axioms for
describing properties of module components.

This is a report on the current state of the semantics of the EML
specification language as in nears completion.  EML is unusual in
being built around a ``real'' programming language having a formal
semantics.  Interesting and complex problems arise both from the
nature of this relationship and from interactions between the
features of the language.},
  NOTE = {\textbf{An extended and improved version is \cite{SannellaDT:eml-gentle-intro97}}}
}

@ARTICLE{SannellaDT:eml-gentle-intro97,
  AUTHOR = {Stefan Kahrs and Donald Sannella and
		 Andrzej Tarlecki},
  TITLE = {The Definition of {E}xtended {ML}: A Gentle
		 Introduction},
  JOURNAL = {Theoretical Computer Science},
  VOLUME = 173,
  PAGES = {445--484},
  YEAR = 1997,
  DVI = {http://homepages.inf.ed.ac.uk/dts/pub/gentle-tcs.dvi},
  POSTSCRIPT = {http://homepages.inf.ed.ac.uk/dts/pub/gentle-tcs.ps},
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/gentle-tcs.pdf},
  ABSTRACT = {Extended ML (EML) is a framework for the formal development of
modular Standard ML (SML) software systems.  Development commences
with a specification of the behaviour required and proceeds via a
sequence of partial solutions until a complete solution, an executable
SML program, is obtained.  All stages in this development process are
expressed in the EML language, an extension of SML with axioms for
describing properties of module components.

This is an overview of the formal definition of the EML language.  To
complement the full technical details presented elsewhere, it provides
an informal explanation of the main ideas, gives the rationale for
certain design decisions, and outlines some of the technical issues
involved.  EML is unusual in being built around a ``real'' programming
language having a formally-defined syntax and semantics.  Interesting
and complex problems arise both from the nature of this relationship
and from interactions between the features of the language.},
  COMMENT = {[This is the final version of
		 \cite{SannellaDT:eml-gentle-intro93}; a close-to-final
		 version of this is: Report ECS-LFCS-95-322, Dept. of
		 Computer Science, Univ. of Edinburgh, 1995.]},
  NOTE = {\textbf{The published version contains two typos:
p461, rule at bottom: second gamma should be gamma';
p462, rule in middle: second premise should start with E}}
}

@INPROCEEDINGS{SannellaDT:eml-interfaces94,
  AUTHOR = {Stefan Kahrs and Donald Sannella and
		 Andrzej Tarlecki},
  TITLE = {Interfaces and {E}xtended {ML}},
  BOOKTITLE = {Proc.\ {ACM} Workshop on Interface Definition
		 Languages},
  LOCATION = {Portland},
  PAGES = {111--118},
  PUBLISHER = {{ACM} {SIGPLAN} Notices 29(8)},
  YEAR = 1994,
  POSTSCRIPT = {http://homepages.inf.ed.ac.uk/dts/pub/interfaces.ps},
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/interfaces.pdf},
  ABSTRACT = {This is a position paper giving our views on the uses and makeup of
module interfaces. The position espoused is inspired by our work on
the Extended ML (EML) formal software development framework and by
ideas in the algebraic foundations of specification and formal
development. The present state of interfaces in EML is outlined and
set in the context of plans for a more general EML-like framework with
axioms in interfaces taken from an arbitrary logical system formulated
as an \emph{institution}. Some more speculative plans are sketched
concerning the simultaneous use of multiple institutions in
specification and development.}
}

@TECHREPORT{SannellaDT:eml-definition94,
  AUTHOR = {Stefan Kahrs and Donald Sannella and
		 Andrzej Tarlecki},
  TITLE = {The Definition of {E}xtended {ML}},
  INSTITUTION = {University of Edinburgh},
  TYPE = {Report},
  NUMBER = {{ECS}-{LFCS}-94-300},
  YEAR = 1994,
  POSTSCRIPT = {http://homepages.inf.ed.ac.uk/dts/pub/eml.ps},
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/eml.pdf},
  ABSTRACT = {This document formally defines the syntax and semantics of the
Extended ML language.  It is based directly on the published semantics
of Standard ML in an attempt to ensure compatibility between the two
languages.},
  COMMENT = {[Version 1; a later version is \cite{SannellaDT:eml-definition97}.]}
}

@UNPUBLISHED{SannellaDT:eml-definition97,
  AUTHOR = {Stefan Kahrs and Donald Sannella and
		 Andrzej Tarlecki},
  TITLE = {The Definition of {E}xtended {ML}, version 1.21},
  YEAR = 1997,
  DVI = {http://homepages.inf.ed.ac.uk/dts/pub/eml-final.dvi},
  POSTSCRIPT = {http://homepages.inf.ed.ac.uk/dts/pub/eml-final.ps},
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/eml-final.pdf},
  ABSTRACT = {This document formally defines the syntax and semantics of the
Extended ML language.  It is based directly on the published semantics
of Standard ML in an attempt to ensure compatibility between the two
languages.},
  NOTE = {Revised version of \cite{SannellaDT:eml-definition94}}
}

@INPROCEEDINGS{SannellaDT:eml-reflections98,
  AUTHOR = {Stefan Kahrs and Donald Sannella},
  TITLE = {Reflections on the Design of a
		Specification Language},
  BOOKTITLE = {Proc.\ Intl.\ Colloq.\ on Fundamental
		Approaches to Software Engineering.
		European Joint Conferences on Theory and Practice of
		Software ({ETAPS}'98)},
  LOCATION = {Lisbon},
  PUBLISHER = {Springer},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = 1382,
  PAGES = {154--170},
  YEAR = 1998,
  DVI = {http://homepages.inf.ed.ac.uk/dts/pub/reflections.dvi},
  POSTSCRIPT = {http://homepages.inf.ed.ac.uk/dts/pub/reflections.ps},
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/reflections.pdf},
  ABSTRACT = {We reflect on our experiences from work on the design and semantic
underpinnings of Extended~ML, a specification language which supports
the specification and formal development of Standard~ML programs.  Our
aim is to isolate problems and issues that are intrinsic to the
general enterprise of designing a specification language for use with
a given programming language.  Consequently the lessons learned go far
beyond our original aim of designing a specification language for ML.}
}

@INPROCEEDINGS{SannellaDT:arch-specs98,
  AUTHOR = {Michel Bidoit and Donald Sannella and
		 Andrzej Tarlecki},
  TITLE = {Architectural Specifications in {CASL}},
  BOOKTITLE = {Proc.\ 7th Intl.\ Conference on Algebraic Methodology and
  Software Technology (AMAST'98)},
  LOCATION = {Manaus},
  PUBLISHER = {Springer},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = 1548,
  PAGES = {341--357},
  YEAR = 1999,
  DVI = {http://homepages.inf.ed.ac.uk/dts/pub/archs-amast.dvi},
  POSTSCRIPT = {http://homepages.inf.ed.ac.uk/dts/pub/archs-amast.ps},
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/archs-amast.pdf},
  ABSTRACT = {One of the novel features of CASL, the Common Algebraic
Specification Language, is the provision of so-called architectural
specifications for describing the modular structure of software
systems.  A discussion of refinement of CASL specifications
provides the setting for a presentation of the rationale behind
architectural specifications.  This is followed by details of the
features provided in CASL for architectural specifications, hints
concerning their semantics, and simple results justifying their
usefulness in the development process.},
  NOTE = {\textbf{An extended version appeared in \cite{SannellaDT:arch-specs01}}}
}

@ARTICLE{SannellaDT:arch-specs01,
  AUTHOR = {Michel Bidoit and Donald Sannella and
		 Andrzej Tarlecki},
  TITLE = {Architectural Specifications in {CASL}},
  JOURNAL = {Formal Aspects of Computing},
  YEAR = {2002},
  VOLUME = 13,
  PAGES = {252--273},
  DVI = {http://homepages.inf.ed.ac.uk/dts/pub/archs.dvi},
  POSTSCRIPT = {http://homepages.inf.ed.ac.uk/dts/pub/archs.ps},
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/archs.pdf},
  ABSTRACT = {One of the most novel features of CASL, the Common Algebraic
Specification Language, is the provision of so-called architectural
specifications for describing the modular structure of software
systems.  A brief discussion of refinement of CASL specifications
provides the setting for a presentation of the rationale behind
architectural specifications.  This is followed by some details of the
features provided in CASL for architectural specifications, hints
concerning their semantics, and simple results justifying their
usefulness in the development process.},
  COMMENT = {[This is an
extended version of \cite{SannellaDT:arch-specs98} that supercedes
Report ECS-LFCS-99-407, Laboratory for Foundations of Computer Science,
Univ.\ of Edinburgh (1999).]}
}

@INPROCEEDINGS{SannellaDT:cofi99,
  AUTHOR = {Donald Sannella},
  TITLE = {The {C}ommon {F}ramework {I}nitiative for Algebraic
Specification and Development of Software},
  BOOKTITLE = {Proc.\ 3rd Intl.\ Conf.\ on Perspectives of System
Informatics (PSI'99)},
  LOCATION = {Novosibirsk},
  PUBLISHER = {Springer},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = 1755,
  YEAR = 2000,
  PAGES = {1--9},
  DVI = {http://homepages.inf.ed.ac.uk/dts/pub/psi.dvi},
  POSTSCRIPT = {http://homepages.inf.ed.ac.uk/dts/pub/psi.ps},
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/psi.pdf},
  ABSTRACT = {The Common Framework Initiative (CoFI) is an open international
collaboration which aims to provide a common framework for algebraic
specification and development of software.  The central element of the
Common Framework is a specification language called CASL for formal
specification of functional requirements and modular software design
which subsumes many previous algebraic specification languages.  This
paper is a brief summary of past and present work on CoFI.}
}

@ARTICLE{SannellaDT:casl01,
  AUTHOR = {Egidio Astesiano and Michel Bidoit and H{\'e}l{\`e}ne
		Kirchner and Bernd Krieg-Br{\"u}ckner and Peter Mosses
		and Donald Sannella and Andrzej Tarlecki},
  TITLE = {{CASL}: The Common Algebraic Specification Language},
  JOURNAL = {Theoretical Computer Science},
  VOLUME = 286,
  YEAR = 2002,
  PAGES = {153--196},
  DVI = {http://homepages.inf.ed.ac.uk/dts/pub/casl.dvi},
  POSTSCRIPT = {http://homepages.inf.ed.ac.uk/dts/pub/casl.ps},
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/casl.pdf},
  ABSTRACT = {CASL is an expressive language for the formal specification of
functional requirements and modular design of software.  It has been
designed by CoFI, the international Common Framework Initiative for
algebraic specification and development.  It is based on a critical
selection of features that have already been explored in various
contexts, including subsorts, partial functions, first-order logic,
and structured and architectural specifications. CASL should
facilitate interoperability of many existing algebraic prototyping and
verification tools.

This paper gives an overview of the CASL design.  The major issues
that had to be resolved in the design process are indicated, and all
the main concepts and constructs of CASL are briefly explained and
illustrated -- the reader is referred to the CASL Language Summary for
further details.  Some familiarity with the fundamental concepts of
algebraic specification would be advantageous.}
}

@INPROCEEDINGS{SannellaDT:cofi01,
  AUTHOR = {Donald Sannella},
  TITLE = {The {C}ommon {F}ramework {I}nitiative for Algebraic
Specification and Development of Software: Recent Progress},
  BOOKTITLE = {Recent Trends in Algebraic Development Techniques:
Selected Papers from WADT 2001},
  LOCATION = {Genova},
  PUBLISHER = {Springer},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = 2267,
  PAGES = {328--343},
  YEAR = {2001},
  POSTSCRIPT = {http://homepages.inf.ed.ac.uk/dts/pub/wadt2001.ps},
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/wadt2001.pdf},
  ABSTRACT = {The Common Framework Initiative (CoFI) is an open international
collaboration which aims to provide a common framework for algebraic
specification and development of software.  The central element of the
Common Framework is a specification language called CASL for formal
specification of functional requirements and modular software design
which subsumes many previous algebraic specification languages.  This
paper is a brief summary of progress on CoFI during the period
1998-2001, when CoFI received funding from the European Commission
as a Working Group under the Esprit programme.}
}

@INPROCEEDINGS{SannellaDT:unit-testing02,
  AUTHOR = {Patricia D.L. Machado and Donald Sannella},
  TITLE = {Unit Testing for {CASL} Architectural Specifications},
  BOOKTITLE = {Proc.\ 27th Intl.\ Symp.\ on Mathematical
		 Foundations of Computer Science},
  LOCATION = {Warsaw},
  PUBLISHER = {Springer},
  SERIES = {Lecture Notes in Computer Science},
  YEAR = 2002,
  VOLUME = 2420,
  PAGES = {506--518},
  DVI = {http://homepages.inf.ed.ac.uk/dts/pub/mfcs2002.dvi},
  POSTSCRIPT = {http://homepages.inf.ed.ac.uk/dts/pub/mfcs2002.ps},
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/mfcs2002.pdf},
  ABSTRACT = {The problem of testing modular systems against algebraic
specifications is discussed. We focus on systems where the
decomposition into parts is specified by a CASL-style architectural
specification and the parts (\emph{units}) are developed separately,
perhaps by an independent supplier.  We consider how to test such
units without reference to their context of use.  This problem is most
acute for generic units where the particular instantiation cannot be
predicted.}
}

@INPROCEEDINGS{SannellaDT:component-oriented04,
  AUTHOR = {Michel Bidoit and Donald Sannella and Andrzej Tarlecki},
  TITLE = {Toward Component-oriented Formal Software Development: An
	Algebraic Approach},
  BOOKTITLE = {Proc.\ 9th Monterey Workshop, Radical Innovations of
	Software and Systems Engineering in the Future},
  LOCATION = {Venice, October 2002},
  PUBLISHER = {Springer},
  SERIES = {Lecture Notes in Computer Science},
  YEAR = 2004,
  VOLUME = 2941,
  PAGES = {75--90},
  DVI = {http://homepages.inf.ed.ac.uk/dts/pub/monterey.dvi},
  POSTSCRIPT = {http://homepages.inf.ed.ac.uk/dts/pub/monterey.ps},
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/monterey.pdf},
  ABSTRACT = {Component based design and development of software is one of the most
challenging issues in software engineering. In this paper, we adopt a
somewhat simplified view of software components and discuss how they
can be conveniently modeled in a framework that provides a modular
approach to formal software development by means of stepwise
refinements. In particular we take into account an observational
interpretation of requirements specifications and study its impact on
the definition of the semantics of specifications of (parametrized)
components. Our study is carried out in the context of CASL
architectural specifications.}
}

@INPROCEEDINGS{SannellaDT:spec-code-CASL02,
  AUTHOR = {David Aspinall and Donald Sannella},
  TITLE = {From Specifications to Code in {CASL}},
  BOOKTITLE = {Proc.\ 9th Intl.\ Conf.\ on Algebraic Methodology And Software Technology},
  LOCATION = {Reunion},
  PUBLISHER = {Springer},
  SERIES = {LNCS},
  YEAR = 2002,
  VOLUME = 2422,
  PAGES = {1--14},
  DVI = {http://homepages.inf.ed.ac.uk/dts/pub/amast2002.dvi},
  POSTSCRIPT = {http://homepages.inf.ed.ac.uk/dts/pub/amast2002.ps},
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/amast2002.pdf},
  ABSTRACT = {The status of the Common Framework Initiative (CoFI) and the Common
Algebraic Specification Language (CASL) are briefly presented.  One
important outstanding point concerns the relationship between CASL and
programming languages; making a proper connection is obviously central
to the use of CASL specifications for software specification and
development.  Some of the issues involved in making this connection
are discussed.}
}

@ARTICLE{SannellaDT:proof-theory04,
  AUTHOR = {Till Mossakowski and Anne Haxthausen and Donald Sannella and Andrzej Tarlecki},
  TITLE = {{CASL} --- The Common Algebraic Specification Language: Semantics and Proof Theory},
  JOURNAL = {Computing and Informatics},
  VOLUME = 22,
  PAGES = {285--321},
  YEAR = {2003},
  DVI = {http://homepages.inf.ed.ac.uk/dts/pub/cai.dvi},
  POSTSCRIPT = {http://homepages.inf.ed.ac.uk/dts/pub/cai.ps},
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/cai.pdf},
  NOTE = {\textbf{An extended version appeared in \cite{SannellaDT:proof-theory08}}},
  ABSTRACT = {CASL is an expressive specification language that has been
designed to supersede many existing algebraic specification
languages and provide a standard. CASL consists of several
layers, including basic (unstructured) specifications,
structured specifications and architectural specifications
(the latter are used to prescribe the structure of implementations).

We describe an simplified version of the CASL syntax, semantics
and proof calculus at each of these three layers and state the
corresponding soundness and completeness theorems. The layers
are orthogonal in the sense that the semantics of a given layer 
uses that of the previous layer as a ``black box'', and
similarly for the proof calculi. In particular, this means
that CASL can easily be adapted to other logical systems.}
}

@INCOLLECTION{SannellaDT:proof-theory08,
  AUTHOR = {Till Mossakowski and Anne Haxthausen and Donald Sannella and Andrzej Tarlecki},
  TITLE = {{CASL} --- The Common Algebraic Specification Language},
  BOOKTITLE = {Logics of Specification Languages},
  PUBLISHER = {Springer},
  EDITOR = {Dines Bj{\o}rner and Martin Henson},
  YEAR = {2008},
  PAGES = {241--298},
  ABSTRACT = {CASL is an expressive specification language that has been
designed to supersede many existing algebraic specification
languages and provide a standard. CASL consists of several
layers, including basic (unstructured) specifications,
structured specifications and architectural specifications;
the latter are used to prescribe the structure of implementations.

We describe an simplified version of the CASL syntax, semantics
and proof calculus for each of these three layers and state the
corresponding soundness and completeness theorems. The layers
are orthogonal in the sense that the semantics of a given layer 
uses that of the previous layer as a ``black box'', and
similarly for the proof calculi. In particular, this means
that CASL can easily be adapted to other logical systems.

We conclude with a detailed example specification of a warehouse,
which serves to illustrate the application of both CASL and the
proof calculi for the various layers.},
  COMMENT = {[This is an extended version of \cite{SannellaDT:proof-theory04}.]}
}

@INCOLLECTION{SannellaDT:foundations03,
  AUTHOR = {Donald Sannella and Andrzej Tarlecki},
  TITLE = {Foundations},
  BOOKTITLE = {{CASL} User Manual},
  CHAPTER = 10,
  PAGES = {125--129},
  BOOKAUTHOR = {Michel Bidoit and Peter Mosses},
  SERIES = {Lecture Notes in Computer Science},
  PUBLISHER = {Springer},
  VOLUME = 2900,
  YEAR = 2003
}

@INCOLLECTION{SannellaDT:CASL-semantics04,
  AUTHOR = {Donald Sannella and Andrzej {Tarlecki, editors}},
  TITLE = {{CASL} Semantics},
  BOOKTITLE = {{CASL} Reference Manual},
  PART = {III},
  PAGES = {115--274},
  EDITOR = {Peter Mosses},
  SERIES = {Lecture Notes in Computer Science},
  PUBLISHER = {Springer},
  VOLUME = 2960,
  YEAR = 2004
}

@INCOLLECTION{SannellaDT:CASL-semantics-intro04,
  AUTHOR = {Donald Sannella},
  TITLE = {{CASL} Semantics: Introduction},
  BOOKTITLE = {{CASL} Reference Manual},
  CHAPTER = {III.1},
  PAGES = {117--123},
  EDITOR = {Peter Mosses},
  SERIES = {Lecture Notes in Computer Science},
  PUBLISHER = {Springer},
  VOLUME = 2960,
  YEAR = 2004
}

@INCOLLECTION{SannellaDT:CASL-semantics-basic-specs04,
  AUTHOR = {Donald Sannella},
  TITLE = {{CASL} Semantics: Basic Specifications},
  BOOKTITLE = {{CASL} Reference Manual},
  CHAPTER = {III.2},
  PAGES = {125--170},
  EDITOR = {Peter Mosses},
  SERIES = {Lecture Notes in Computer Science},
  PUBLISHER = {Springer},
  VOLUME = 2960,
  YEAR = 2004
}

@INPROCEEDINGS{SannellaDT:casl-refinement04,
  AUTHOR = {Till Mossakowski and Donald Sannella and Andrzej Tarlecki},
  TITLE = {A Simple Refinement Language for {CASL}},
  BOOKTITLE = {Recent Trends in Algebraic Development Techniques:
Selected Papers from WADT 2004},
  LOCATION = {Barcelona},
  PUBLISHER = {Springer},
  SERIES = {LNCS},
  VOLUME = 3423,
  PAGES = {162--185},
  YEAR = 2004,
  DVI = {http://homepages.inf.ed.ac.uk/dts/pub/casl-refinement.dvi},
  POSTSCRIPT = {http://homepages.inf.ed.ac.uk/dts/pub/casl-refinement.ps},
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/casl-refinement.pdf},
  ABSTRACT = {We extend CASL architectural specifications with a simple
refinement language that allows the formalization of developments as
refinement trees.  The essence of the extension is to allow
refinements of unit specifications in CASL architectural specifications.}
}

@ARTICLE{SannellaDT:obs-interp-casl-specs08,
  AUTHOR = {Michel Bidoit and Donald Sannella and Andrzej Tarlecki},
  TITLE = {Observational Interpretation of {CASL} Specifications},
  JOURNAL = {Mathematical Structures in Computer Science},
  VOLUME = {18},
  PAGES = {325--371},
  YEAR = 2008,
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/casl-obs.pdf},
  ABSTRACT = {The way that refinement of individual ``local'' components of a
specification relates to development of a ``global'' system from a
specification of requirements is explored.  Observational
interpretation of specifications and refinements add expressive power
and flexibility while bringing in some subtle problems.  Our study of
these issues is carried out in the context of CASL architectural
specifications.  We introduce a definition of observational
equivalence for CASL models, leading to an observational semantics for
architectural specifications for which we prove important properties.
Overall, this fulfills the long-standing goal of complementing the
standard semantics of CASL specifications with an observational view
that supports observational refinement of specifications in
combination with CASL-style architectural design.},
  COMMENT = {[An early short version was \cite{SannellaDT:global-dev02}.]}
}

@INPROCEEDINGS{SannellaDT:hope80,
  AUTHOR = {Rod Burstall and David MacQueen and
		 Donald Sannella},
  TITLE = {{HOPE}: An Experimental Applicative Language},
  BOOKTITLE = {Proc.\ 1980 {LISP} Conference},
  LOCATION = {Stanford},
  YEAR = 1980,
  PAGES = {136--143},
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/hope.pdf},
  ABSTRACT = {An applicative language called HOPE is described and discussed.  The
underlying goal of the design and implementation effort was to produce
a very simple programming language which encourages the construction
of clear and manipulable programs.  HOPE does not include an
assignment statement; this is felt to be an important simplification.
The user may freely define his own data types, without the need to
devise a complicated encoding in terms of low-level types.  The
language is very strongly typed, and as implemented it incorporates a
typechecker which handles polymorphic types and overloaded operators.
Functions are defined by a set of recursion equations; the left-hand
side of each equation includes a pattern used to determine which
equation to use for a given argument.  The availability of arbitrary
higher-order types allows functions to be defined which ``package''
recursion.  Lazily-evaluated lists are provided, allowing the use of
infinite lists which could be used to provide interactive input/output
and concurrency.  HOPE also includes a simple modularisation facility
which may be used to protect the implementation of an abstract data
type.}
}

@ARTICLE{SannellaDT:functional-programming-intro87,
  AUTHOR = {Martin Wirsing and Donald Sannella},
  TITLE = {Une Introduction {\`a} la Programmation Fontionnelle:
		 {HOPE} et {ML}},
  JOURNAL = {Technique et Science Informatiques},
  VOLUME = 6,
  PAGES = {517--525},
  YEAR = 1987,
  COMMENT = {[A terrible english translation is: Introduction to Functional
		 Programming: {HOPE} and {ML}.  \emph{Technology and
		 Science of Informatics} 6:693--700 (1989).]}
}

@BOOK{SannellaDT:WADT88,
  AUTHOR = {Donald Sannella and Andrzej Tarlecki},
  TITLE = {Recent Trends in Data Type Specification:
5th Workshop on Specification of Abstract Data Types --- Selected Papers},
  SERIES = {Lecture Notes in Computer Science},
  PUBLISHER = {Springer},
  VOLUME = 332,
  YEAR = 1988
}

@INPROCEEDINGS{SannellaDT:proving-logic-programs88,
  AUTHOR = {Alan Bundy and Donald Sannella and Roberto Desimone
		 and Fausto Giunchiglia and Frank van Harmelen and
		 Jane Hesketh and Peter Madden and Alan Smaill and
		 Andrew Stevens and Lincoln Wallen},
  TITLE = {Proving Properties of Logic Programs: A Progress
		 Report},
  BOOKTITLE = {Proc.\ 1988 Alvey Technical Conference},
  PAGES = {153--156},
  YEAR = 1988
}

@INCOLLECTION{SannellaDT:formal-methods-survey93,
  AUTHOR = {Donald Sannella},
  TITLE = {A Survey of Formal Software Development Methods},
  BOOKTITLE = {Software Engineering: A European Perspective},
  PUBLISHER = {{IEEE} Computer Society Press},
  EDITOR = {Richard Thayer and Andrew McGettrick},
  COMMENT = {[Originally published as report ECS-LFCS-88-56,
		 Dept. of Computer Science, Univ. of Edinburgh, 1988.]},
  PAGES = {281--297},
  YEAR = 1993,
  POSTSCRIPT = {http://homepages.inf.ed.ac.uk/dts/pub/survey.ps},
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/survey.pdf},
  ABSTRACT = {This paper is a survey of the state of the art in 1988 of research on
methods for formal software development.}
}

@TECHREPORT{SannellaDT:exam-questions88,
  AUTHOR = {Donald Sannella},
  TITLE = {Edinburgh {U}niversity Postgraduate Examination
		 Questions in Computation Theory, 1978--1988},
  INSTITUTION = {University of Edinburgh},
  TYPE = {Report},
  NUMBER = {{ECS}-{LFCS}-88-64},
  YEAR = 1988
}

@INPROCEEDINGS{SannellaDT:modular-rule-bases89,
  AUTHOR = {Jaume Agust{\'\i} and Carlos Sierra and
		 Donald Sannella},
  TITLE = {Adding Generic Modules to Flat Rule-Based Languages:
		 A Low-Cost Approach},
  LOCATION = {Charlotte, North Carolina},
  BOOKTITLE = {Proc.\ 4th Intl.\ Symp.\ on Methodologies for
		 Intelligent Systems},
  PUBLISHER = {North Holland},
  PAGES = {43--51},
  YEAR = 1989
}

@INPROCEEDINGS{SannellaDT:modular-prolog87,
  AUTHOR = {Donald Sannella and Lincoln Wallen},
  TITLE = {A Calculus for the Construction of Modular {P}rolog
		 Programs},
  BOOKTITLE = {Proc.\ 1987 {IEEE} Symp.\ on Logic Programming},
  LOCATION = {San Francisco},
  PAGES = {368--378},
  YEAR = 1987,
  NOTE = {\textbf{Extended abstract; the final full version of this is \cite{SannellaDT:modular-prolog92}}},
  ABSTRACT = {We present a module language for Prolog based on the theory of
modularity underlying the Standard ML module system.  The calculus
supports the construction of hierarchically-structured programs from
parameterised components and provides a form of structural data
abstraction.  The system has a formal semantics which translates
modular programs into conventional programs.}
}

@ARTICLE{SannellaDT:modular-prolog92,
  AUTHOR = {Donald Sannella and Lincoln Wallen},
  TITLE = {A Calculus for the Construction of Modular {P}rolog
		 Programs},
  JOURNAL = {Journal of Logic Programming},
  VOLUME = 12,
  YEAR = 1992,
  PAGES = {147--177},
  ABSTRACT = {We present a module language for Prolog based on the theory of
modularity underlying the Standard ML module system.  The language
supports the construction of hierarchically-structured programs from
parameterised components and provides a form of structural data
abstraction.  A formal semantics is given for the system which
translates modular programs into conventional programs.},
  COMMENT = {[An extended abstract of this is
		 \cite{SannellaDT:modular-prolog87}.]}
}

@INPROCEEDINGS{SannellaDT:future-of-TCS97,
  AUTHOR = {Donald Sannella},
  TITLE = {What Does the Future Hold for Theoretical Computer
		  	Science?},
  BOOKTITLE = {Proc.\ 7th Intl.\ Joint Conf.\ on Theory and
		  	Practice of Software Development ({TAPSOFT}'97)},
  LOCATION = {Lille},
  PUBLISHER = {Springer},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = 1214,
  PAGES = {15--19},
  YEAR = 1997,
  DVI = {http://homepages.inf.ed.ac.uk/dts/pub/tapsoft97.dvi},
  POSTSCRIPT = {http://homepages.inf.ed.ac.uk/dts/pub/tapsoft97.ps},
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/tapsoft97.pdf},
  ABSTRACT = {Prospects for research in theoretical computer science are discussed.
The maintenance of a genuine link between theory and practice is seen
as key to the future health of both.}
}

@ARTICLE{SannellaDT:burstall-festschrift02,
  AUTHOR = {David Rydeheard and Donald Sannella},
  TITLE = {Preface to a Collection of Papers and Memoirs Celebrating the Contribution of {R}od {B}urstall to Advances in {C}omputer {S}cience},
  JOURNAL = {Formal Aspects of Computing},
  VOLUME = 13,
  YEAR = 2002,
  PAGES = {187--193},
  DVI = {http://homepages.inf.ed.ac.uk/dts/pub/burstall.dvi},
  POSTSCRIPT = {http://homepages.inf.ed.ac.uk/dts/pub/burstall.ps},
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/burstall.pdf},
  ABSTRACT = {In this Preface, we attempt to summarize Rod Burstall's scientific achievements.
In addition, we describe the personal style and enthusiasm that Rod has brought
to the subject.}
}

@INPROCEEDINGS{SannellaDT:mrg-overview04,
  AUTHOR = {David Aspinall and Stephen Gilmore and Martin Hofmann and Donald Sannella and Ian Stark},
  TITLE = {Mobile Resource Guarantees for Smart Devices},
  BOOKTITLE = {Proc.\ Intl.\ Workshop on Construction and Analysis of Safe, Secure and Interoperable Smart Devices (CASSIS 2004)},
  LOCATION = {Marseille},
  PUBLISHER = {Springer},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = 3362,
  YEAR = 2005,
  PAGES = {1--26},
  DVI = {http://homepages.inf.ed.ac.uk/dts/pub/cassis2004.dvi},
  POSTSCRIPT = {http://homepages.inf.ed.ac.uk/dts/pub/cassis2004.ps},
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/cassis2004.pdf},
  ABSTRACT = {We present the Mobile Resource Guarantees framework: a system for
ensuring that downloaded programs are free from run-time violations of
resource bounds.  Certificates are attached to code in the form of
efficiently checkable proofs of resource bounds; in contrast to
cryptographic certificates of code origin, these are independent of
trust networks.  A novel programming language with resource
constraints encoded in function types is used to streamline the
generation of proofs of resource usage.}
}

@INPROCEEDINGS{SannellaDT:mrg-summary05,
  AUTHOR = {Donald Sannella and Martin Hofmann and David Aspinall and Stephen Gilmore and Ian Stark and Lennart Beringer and Hans-Wolfgang Loidl and Kenneth MacKenzie and Alberto Momigliano and Olha Shkaravska},
  TITLE = {Mobile Resource Guarantees},
  BOOKTITLE = {Trends in Functional Programming},
  PUBLISHER = {Intellect},
  VOLUME = 6,
  PAGES = {211--226},
  YEAR = 2007,
  DVI = {http://homepages.inf.ed.ac.uk/dts/pub/mrg-summary.dvi},
  POSTSCRIPT = {http://homepages.inf.ed.ac.uk/dts/pub/mrg-summary.ps},
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/mrg-summary.pdf},
  ABSTRACT = {The Mobile Resource Guarantees (MRG) project has developed a
proof-carrying-code infrastructure for certifying resource bounds of
mobile code.  Key components of this infrastructure are a certifying
compiler for a high-level language, a hierarchy of program logics,
tailored for reasoning about resource consumption, and an embedding of
the logics into a theorem prover. In this paper, we give an overview
of the project's results, discuss the lessons learnt from it and
introduce follow-up work in new projects that will build on these
results.}
}

@INPROCEEDINGS{SannellaDT:request10,
  AUTHOR = {David Aspinall and Robert Atkey and Kenneth MacKenzie and Donald Sannella},
  TITLE = {Symbolic and Analytical Techniques for Resource Analysis of
	{Java} Bytecode},
  BOOKTITLE = {Proc.\ 5th Symp.\ on Trustworthy Global Computing (TGC 2010)},
  LOCATION = {Munich},
  PUBLISHER = {Springer},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = 6084,
  PAGES = {1--22},
  YEAR = 2010,
  PDF = {http://homepages.inf.ed.ac.uk/dts/pub/tgc2010.pdf},
  ABSTRACT = {Recent work in resource analysis has translated the idea of amortised
resource analysis to imperative languages using a program logic that
allows mixing of assertions about heap shapes, in the tradition of
separation logic, and assertions about consumable
resources. Separately, polyhedral methods have been used to calculate
bounds on numbers of iterations in loop-based programs.
We are attempting to combine these ideas to deal with Java programs
involving both data structures and loops, focusing on the bytecode
level rather than on source code.}
}