\newcommand{\etalchar}[1]{$^{#1}$}
\begin{thebibliography}{AGH{\etalchar{+}}05}

\bibitem[AAMS10]{SannellaDT:request10}
David Aspinall, Robert Atkey, Kenneth MacKenzie, and Donald Sannella.
\newblock Symbolic and analytical techniques for resource analysis of {Java}
  bytecode.
\newblock In {\em Proc.\ 5th Symp.\ on Trustworthy Global Computing (TGC
  2010)}, volume 6084 of {\em Lecture Notes in Computer Science}, pages 1--22.
  Springer, 2010.

\bibitem[ABK{\etalchar{+}}02]{SannellaDT:casl01}
Egidio Astesiano, Michel Bidoit, H{\'e}l{\`e}ne Kirchner, Bernd
  Krieg-Br{\"u}ckner, Peter Mosses, Donald Sannella, and Andrzej Tarlecki.
\newblock {CASL}: The common algebraic specification language.
\newblock {\em Theoretical Computer Science}, 286:153--196, 2002.

\bibitem[AGH{\etalchar{+}}05]{SannellaDT:mrg-overview04}
David Aspinall, Stephen Gilmore, Martin Hofmann, Donald Sannella, and Ian
  Stark.
\newblock Mobile resource guarantees for smart devices.
\newblock In {\em Proc.\ Intl.\ Workshop on Construction and Analysis of Safe,
  Secure and Interoperable Smart Devices (CASSIS 2004)}, volume 3362 of {\em
  Lecture Notes in Computer Science}, pages 1--26. Springer, 2005.

\bibitem[AS02]{SannellaDT:spec-code-CASL02}
David Aspinall and Donald Sannella.
\newblock From specifications to code in {CASL}.
\newblock In {\em Proc.\ 9th Intl.\ Conf.\ on Algebraic Methodology And
  Software Technology}, volume 2422 of {\em LNCS}, pages 1--14. Springer, 2002.

\bibitem[AS15]{SannellaDT:avocs15}
Robert Atkey and Donald Sannella.
\newblock {ThreadSafe}: Static analysis for {Java} concurrency.
\newblock {\em Electronic Communications of the EASST}, 72, 2015.

\bibitem[ASS89]{SannellaDT:modular-rule-bases89}
Jaume Agust{\'\i}, Carlos Sierra, and Donald Sannella.
\newblock Adding generic modules to flat rule-based languages: A low-cost
  approach.
\newblock In {\em Proc.\ 4th Intl.\ Symp.\ on Methodologies for Intelligent
  Systems}, pages 43--51. North Holland, 1989.

\bibitem[BKL{\etalchar{+}}91]{SannellaDT:compass-bibliography91}
Michel Bidoit, Hans-J{\"o}rg Kreowski, Pierre Lescanne, Fernando Orejas, and
  Donald Sannella, editors.
\newblock {\em Algebraic System Specification and Development: A Survey and
  Annotated Bibliography}, volume 501 of {\em Lecture Notes in Computer
  Science}.
\newblock Springer, 1991.

\bibitem[BMS80]{SannellaDT:hope80}
Rod Burstall, David MacQueen, and Donald Sannella.
\newblock {HOPE}: An experimental applicative language.
\newblock In {\em Proc.\ 1980 {LISP} Conference}, pages 136--143, 1980.

\bibitem[BSD{\etalchar{+}}88]{SannellaDT:proving-logic-programs88}
Alan Bundy, Donald Sannella, Roberto Desimone, Fausto Giunchiglia, Frank van
  Harmelen, Jane Hesketh, Peter Madden, Alan Smaill, Andrew Stevens, and
  Lincoln Wallen.
\newblock Proving properties of logic programs: A progress report.
\newblock In {\em Proc.\ 1988 Alvey Technical Conference}, pages 153--156,
  1988.

\bibitem[BST99]{SannellaDT:arch-specs98}
Michel Bidoit, Donald Sannella, and Andrzej Tarlecki.
\newblock Architectural specifications in {CASL}.
\newblock In {\em Proc.\ 7th Intl.\ Conference on Algebraic Methodology and
  Software Technology (AMAST'98)}, volume 1548 of {\em Lecture Notes in
  Computer Science}, pages 341--357. Springer, 1999.
\newblock \textbf{An extended version appeared in
  \cite{SannellaDT:arch-specs01}}.

\bibitem[BST02a]{SannellaDT:arch-specs01}
Michel Bidoit, Donald Sannella, and Andrzej Tarlecki.
\newblock Architectural specifications in {CASL}.
\newblock {\em Formal Aspects of Computing}, 13:252--273, 2002.

\bibitem[BST02b]{SannellaDT:global-dev02}
Michel Bidoit, Donald Sannella, and Andrzej Tarlecki.
\newblock Global development via local observational construction steps.
\newblock In {\em Proc.\ 27th Intl.\ Symp.\ on Mathematical Foundations of
  Computer Science}, volume 2420 of {\em Lecture Notes in Computer Science},
  pages 1--24. Springer, 2002.
\newblock \textbf{An extended version appeared in
  \cite{SannellaDT:obs-interp-casl-specs08}}.

\bibitem[BST04]{SannellaDT:component-oriented04}
Michel Bidoit, Donald Sannella, and Andrzej Tarlecki.
\newblock Toward component-oriented formal software development: An algebraic
  approach.
\newblock In {\em Proc.\ 9th Monterey Workshop, Radical Innovations of Software
  and Systems Engineering in the Future}, volume 2941 of {\em Lecture Notes in
  Computer Science}, pages 75--90. Springer, 2004.

\bibitem[BST08]{SannellaDT:obs-interp-casl-specs08}
Michel Bidoit, Donald Sannella, and Andrzej Tarlecki.
\newblock Observational interpretation of {CASL} specifications.
\newblock {\em Mathematical Structures in Computer Science}, 18:325--371, 2008.

\bibitem[HKS03]{SannellaDT:simulation-relations03}
Jo~Hannay, {Shin-ya} Katsumata, and Donald Sannella.
\newblock Semantic and syntactic approaches to simulation relations.
\newblock In {\em Proc.\ 28th Intl.\ Symp.\ on Mathematical Foundations of
  Computer Science}, volume 2747 of {\em Lecture Notes in Computer Science},
  pages 68--91. Springer, 2003.

\bibitem[HLST00]{SannellaDT:constructive-refinement00}
Furio Honsell, John Longley, Donald Sannella, and Andrzej Tarlecki.
\newblock Constructive data refinement in typed lambda calculus.
\newblock In {\em Proc.\ 3rd Intl.\ Conf.\ on Foundations of Software Science
  and Computation Structures. European Joint Conferences on Theory and Practice
  of Software ({ETAPS} 2000)}, volume 1784 of {\em Lecture Notes in Computer
  Science}, pages 161--176. Springer, 2000.

\bibitem[HS95]{SannellaDT:behavioural-abstraction-hol95}
Martin Hofmann and Donald Sannella.
\newblock On behavioural abstraction and behavioural satisfaction in
  higher-order logic.
\newblock In {\em Proc.\ 20th Colloq.\ on Trees in Algebra and Programming.
  Intl.\ Joint Conf.\ on Theory and Practice of Software Development
  ({TAPSOFT}'95)}, volume 915 of {\em Lecture Notes in Computer Science}, pages
  247--261. Springer, 1995.
\newblock \textbf{The final full version of this is
  \cite{SannellaDT:behavioural-abstraction-hol96}}.

\bibitem[HS96]{SannellaDT:behavioural-abstraction-hol96}
Martin Hofmann and Donald Sannella.
\newblock On behavioural abstraction and behavioural satisfaction in
  higher-order logic.
\newblock {\em Theoretical Computer Science}, 167:3--45, 1996.

\bibitem[HS99]{SannellaDT:prelogical-relations99}
Furio Honsell and Donald Sannella.
\newblock Pre-logical relations.
\newblock In {\em Proc.\ Computer Science Logic, CSL'99}, volume 1683 of {\em
  Lecture Notes in Computer Science}, pages 546--561. Springer, 1999.
\newblock \textbf{The final full version of this is
  \cite{SannellaDT:prelogical-relations00}}.

\bibitem[HS02]{SannellaDT:prelogical-relations00}
Furio Honsell and Donald Sannella.
\newblock Prelogical relations.
\newblock {\em Information and Computation}, 178:23--43, 2002.

\bibitem[HST89a]{SannellaDT:logic-representation89}
Robert Harper, Donald Sannella, and Andrzej Tarlecki.
\newblock Logic representation in {LF}.
\newblock In {\em Proc.\ 3rd Summer Conf.\ on Category Theory and Computer
  Science}, volume 389 of {\em Lecture Notes in Computer Science}, pages
  250--272. Springer, 1989.

\bibitem[HST89b]{SannellaDT:structure-representation89}
Robert Harper, Donald Sannella, and Andrzej Tarlecki.
\newblock Structure and representation in {LF}.
\newblock In {\em Proc.\ 4th {IEEE} Symp.\ on Logic in Computer Science}, pages
  226--237, 1989.
\newblock \textbf{Extended abstract; the final full version of this is
  \cite{SannellaDT:structured-presentations94}}.

\bibitem[HST89c]{SannellaDT:structure-representation89a}
Robert Harper, Donald Sannella, and Andrzej Tarlecki.
\newblock Structure and representation in {LF}.
\newblock In {\em Proc.\ 1989 Workshop on Programming Logic}, pages 232--257,
  1989.
\newblock \textbf{Extended abstract; the final full version of this is
  \cite{SannellaDT:structured-presentations94}}.

\bibitem[HST94]{SannellaDT:structured-presentations94}
Robert Harper, Donald Sannella, and Andrzej Tarlecki.
\newblock Structured presentations and logic representations.
\newblock {\em Annals of Pure and Applied Logic}, 67:113--160, 1994.

\bibitem[KBS91]{SannellaDT:spectral91}
Bernd Krieg-Br{\"u}ckner and Donald Sannella.
\newblock Structuring specifications in-the-large and in-the-small:
  Higher-order functions, dependent types and inheritance in {SPECTRAL}.
\newblock In {\em Proc.\ Colloq.\ on Combining Paradigms for Software
  Development. Intl.\ Joint Conf.\ on Theory and Practice of Software
  Development ({TAPSOFT}'91)}, volume 494 of {\em Lecture Notes in Computer
  Science}, pages 103--120. Springer, 1991.

\bibitem[KS98]{SannellaDT:eml-reflections98}
Stefan Kahrs and Donald Sannella.
\newblock Reflections on the design of a specification language.
\newblock In {\em Proc.\ Intl.\ Colloq.\ on Fundamental Approaches to Software
  Engineering. European Joint Conferences on Theory and Practice of Software
  ({ETAPS}'98)}, volume 1382 of {\em Lecture Notes in Computer Science}, pages
  154--170. Springer, 1998.

\bibitem[KST94a]{SannellaDT:eml-definition94}
Stefan Kahrs, Donald Sannella, and Andrzej Tarlecki.
\newblock The definition of {E}xtended {ML}.
\newblock Report {ECS}-{LFCS}-94-300, University of Edinburgh, 1994.

\bibitem[KST94b]{SannellaDT:eml-interfaces94}
Stefan Kahrs, Donald Sannella, and Andrzej Tarlecki.
\newblock Interfaces and {E}xtended {ML}.
\newblock In {\em Proc.\ {ACM} Workshop on Interface Definition Languages},
  pages 111--118. {ACM} {SIGPLAN} Notices 29(8), 1994.

\bibitem[KST94c]{SannellaDT:eml-gentle-intro93}
Stefan Kahrs, Donald Sannella, and Andrzej Tarlecki.
\newblock The semantics of {E}xtended {ML}: A gentle introduction.
\newblock In {\em Proc.\ Intl.\ Workshop on Semantics of Specification
  Languages}, Workshops in Computing, pages 186--215. Springer, 1994.
\newblock \textbf{An extended and improved version is
  \cite{SannellaDT:eml-gentle-intro97}}.

\bibitem[KST97a]{SannellaDT:eml-gentle-intro97}
Stefan Kahrs, Donald Sannella, and Andrzej Tarlecki.
\newblock The definition of {E}xtended {ML}: A gentle introduction.
\newblock {\em Theoretical Computer Science}, 173:445--484, 1997.
\newblock \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}.

\bibitem[KST97b]{SannellaDT:eml-definition97}
Stefan Kahrs, Donald Sannella, and Andrzej Tarlecki.
\newblock The definition of {E}xtended {ML}, version 1.21.
\newblock Revised version of \cite{SannellaDT:eml-definition94}, 1997.

\bibitem[MHST03]{SannellaDT:proof-theory04}
Till Mossakowski, Anne Haxthausen, Donald Sannella, and Andrzej Tarlecki.
\newblock {CASL} --- the common algebraic specification language: Semantics and
  proof theory.
\newblock {\em Computing and Informatics}, 22:285--321, 2003.
\newblock \textbf{An extended version appeared in
  \cite{SannellaDT:proof-theory08}}.

\bibitem[MHST08]{SannellaDT:proof-theory08}
Till Mossakowski, Anne Haxthausen, Donald Sannella, and Andrzej Tarlecki.
\newblock {CASL} --- the common algebraic specification language.
\newblock In Dines Bj{\o}rner and Martin Henson, editors, {\em Logics of
  Specification Languages}, pages 241--298. Springer, 2008.

\bibitem[MPST14]{SannellaDT:parchments14}
Till Mossakowski, Wies{\l}aw Paw{\l}owski, Donald Sannella, and Andrzej
  Tarlecki.
\newblock Parchments for {CafeOBJ} logics.
\newblock In {\em Specification, Algebra, and Software: Essays Dedicated to
  Kokichi Futatsugi}, volume 8373 of {\em Lecture Notes in Computer Science},
  pages 66--91. Springer, 2014.

\bibitem[MS85]{SannellaDT:completeness85}
David MacQueen and Donald Sannella.
\newblock Completeness of proof systems for equational specifications.
\newblock {\em {IEEE} Trans.\ on Software Engineering}, {SE}-11(5):454--461,
  1985.

\bibitem[MS02]{SannellaDT:unit-testing02}
Patricia~D.L. Machado and Donald Sannella.
\newblock Unit testing for {CASL} architectural specifications.
\newblock In {\em Proc.\ 27th Intl.\ Symp.\ on Mathematical Foundations of
  Computer Science}, volume 2420 of {\em Lecture Notes in Computer Science},
  pages 506--518. Springer, 2002.

\bibitem[MST04]{SannellaDT:casl-refinement04}
Till Mossakowski, Donald Sannella, and Andrzej Tarlecki.
\newblock A simple refinement language for {CASL}.
\newblock In {\em Recent Trends in Algebraic Development Techniques: Selected
  Papers from WADT 2004}, volume 3423 of {\em LNCS}, pages 162--185. Springer,
  2004.

\bibitem[MST15]{SannellaDT:alg-constructions15}
Grzegorz Marczy{\'n}ski, Donald Sannella, and Andrzej Tarlecki.
\newblock Algebraic constructions: a simple framework for complex dependencies
  and parameterisation.
\newblock {\em International Journal of Software and Informatics},
  9(2):117--139, 2015.

\bibitem[PPST00]{SannellaDT:lax-logical-relations00}
Gordon Plotkin, John Power, Donald Sannella, and Robert Tennent.
\newblock Lax logical relations.
\newblock In {\em Proc.\ 27th Intl.\ Colloq.\ on Automata, Languages and
  Programming}, volume 1853 of {\em Lecture Notes in Computer Science}, pages
  85--102. Springer, 2000.

\bibitem[RS02]{SannellaDT:burstall-festschrift02}
David Rydeheard and Donald Sannella.
\newblock Preface to a collection of papers and memoirs celebrating the
  contribution of {R}od {B}urstall to advances in {C}omputer {S}cience.
\newblock {\em Formal Aspects of Computing}, 13:187--193, 2002.

\bibitem[San82]{SannellaDT:phd82}
Donald Sannella.
\newblock {\em Semantics, Implementation and Pragmatics of {C}lear, a Program
  Specification Language}.
\newblock PhD thesis, Department of Computer Science, University of Edinburgh,
  1982.
\newblock Report CST-17-82.

\bibitem[San83]{SannellaDT:behavioural-abstraction83}
Donald Sannella.
\newblock Behavioural abstraction and algebraic specification.
\newblock In {\em Proc.\ 1983 Workshop on Semantics of Programming Languages},
  pages 153--166, 1983.

\bibitem[San84]{SannellaDT:clear-semantics84}
Donald Sannella.
\newblock A set-theoretic semantics for {C}lear.
\newblock {\em Acta Informatica}, 21:443--472, 1984.

\bibitem[San87]{SannellaDT:eml-tutorial87}
Donald Sannella.
\newblock Formal specification of {ML} programs.
\newblock In {\em Jornadas Rank Xerox Sobre Inteligencia Artificial
  Razonamiento Automatizado}, pages 79--98, 1987.

\bibitem[San88a]{SannellaDT:lfcs-newsletter-survey88}
Donald Sannella.
\newblock Algebraic specification and formal program development: Motivation,
  present state and future prospects.
\newblock {\em {LFCS} Newsletter}, 1:7--10, 1988.

\bibitem[San88b]{SannellaDT:exam-questions88}
Donald Sannella.
\newblock Edinburgh {U}niversity postgraduate examination questions in
  computation theory, 1978--1988.
\newblock Report {ECS}-{LFCS}-88-64, University of Edinburgh, 1988.

\bibitem[San91]{SannellaDT:eml-working-programmer91}
Donald Sannella.
\newblock Formal program development in {E}xtended {ML} for the working
  programmer.
\newblock In {\em Proc.\ 3rd {BCS}/{FACS} Workshop on Refinement}, Workshops in
  Computing, pages 99--130. Springer, 1991.

\bibitem[San93]{SannellaDT:formal-methods-survey93}
Donald Sannella.
\newblock A survey of formal software development methods.
\newblock In Richard Thayer and Andrew McGettrick, editors, {\em Software
  Engineering: A European Perspective}, pages 281--297. {IEEE} Computer Society
  Press, 1993.

\bibitem[San97]{SannellaDT:future-of-TCS97}
Donald Sannella.
\newblock What does the future hold for theoretical computer science?
\newblock In {\em Proc.\ 7th Intl.\ Joint Conf.\ on Theory and Practice of
  Software Development ({TAPSOFT}'97)}, volume 1214 of {\em Lecture Notes in
  Computer Science}, pages 15--19. Springer, 1997.

\bibitem[San00a]{SannellaDT:refinement99}
Donald Sannella.
\newblock Algebraic specification and program development by stepwise
  refinement.
\newblock In {\em Proc.\ 9th Intl.\ Workshop on Logic-based Program Synthesis
  and Transformation, {LOPSTR}'99}, volume 1817 of {\em Lecture Notes in
  Computer Science}, pages 1--9. Springer, 2000.

\bibitem[San00b]{SannellaDT:cofi99}
Donald Sannella.
\newblock The {C}ommon {F}ramework {I}nitiative for algebraic specification and
  development of software.
\newblock In {\em Proc.\ 3rd Intl.\ Conf.\ on Perspectives of System
  Informatics (PSI'99)}, volume 1755 of {\em Lecture Notes in Computer
  Science}, pages 1--9. Springer, 2000.

\bibitem[San01]{SannellaDT:cofi01}
Donald Sannella.
\newblock The {C}ommon {F}ramework {I}nitiative for algebraic specification and
  development of software: Recent progress.
\newblock In {\em Recent Trends in Algebraic Development Techniques: Selected
  Papers from WADT 2001}, volume 2267 of {\em Lecture Notes in Computer
  Science}, pages 328--343. Springer, 2001.

\bibitem[San04a]{SannellaDT:CASL-semantics-basic-specs04}
Donald Sannella.
\newblock {CASL} semantics: Basic specifications.
\newblock In Peter Mosses, editor, {\em {CASL} Reference Manual}, volume 2960
  of {\em Lecture Notes in Computer Science}, chapter III.2, pages 125--170.
  Springer, 2004.

\bibitem[San04b]{SannellaDT:CASL-semantics-intro04}
Donald Sannella.
\newblock {CASL} semantics: Introduction.
\newblock In Peter Mosses, editor, {\em {CASL} Reference Manual}, volume 2960
  of {\em Lecture Notes in Computer Science}, chapter III.1, pages 117--123.
  Springer, 2004.

\bibitem[SB83]{SannellaDT:structured-theories83}
Donald Sannella and Rod Burstall.
\newblock Structured theories in {LCF}.
\newblock In {\em Proc.\ 8th Colloq.\ on Trees in Algebra and Programming},
  volume 159 of {\em Lecture Notes in Computer Science}, pages 377--391.
  Springer, 1983.

\bibitem[SHA{\etalchar{+}}07]{SannellaDT:mrg-summary05}
Donald Sannella, Martin Hofmann, David Aspinall, Stephen Gilmore, Ian Stark,
  Lennart Beringer, Hans-Wolfgang Loidl, Kenneth MacKenzie, Alberto Momigliano,
  and Olha Shkaravska.
\newblock Mobile resource guarantees.
\newblock In {\em Trends in Functional Programming}, volume~6, pages 211--226.
  Intellect, 2007.

\bibitem[SST92]{SannellaDT:parameterisation-revisited92}
Donald Sannella, Stefan Soko{\l}owski, and Andrzej Tarlecki.
\newblock Toward formal development of programs from algebraic specifications:
  Parameterisation revisited.
\newblock {\em Acta Informatica}, 29(8):689--736, 1992.

\bibitem[ST84]{SannellaDT:specs-arbitrary-institution84}
Donald Sannella and Andrzej Tarlecki.
\newblock Building specifications in an arbitrary institution.
\newblock In {\em Proc.\ Intl.\ Symp.\ on Semantics of Data Types}, volume 173
  of {\em Lecture Notes in Computer Science}, pages 337--356. Springer, 1984.
\newblock \textbf{An extended and improved version is
  \cite{SannellaDT:specs-arbitrary-institution88}}.

\bibitem[ST85a]{SannellaDT:observational-equivalence85}
Donald Sannella and Andrzej Tarlecki.
\newblock On observational equivalence and algebraic specification.
\newblock In {\em Proc.\ 10th Colloq.\ on Trees in Algebra and Programming.
  Intl.\ Joint Conf.\ on Theory and Practice of Software Development
  ({TAPSOFT}'85)}, volume 185 of {\em Lecture Notes in Computer Science}, pages
  308--322. Springer, 1985.
\newblock \textbf{Extended abstract; the final full version of this is
  \cite{SannellaDT:observational-equivalence87}}.

\bibitem[ST85b]{SannellaDT:eml-intro85}
Donald Sannella and Andrzej Tarlecki.
\newblock Program specification and development in {S}tandard {ML}.
\newblock In {\em Proc.\ 12th {ACM} Symp.\ on Principles of Programming
  Languages}, pages 67--77, 1985.

\bibitem[ST85c]{SannellaDT:thoughts85}
Donald Sannella and Andrzej Tarlecki.
\newblock Some thoughts on algebraic specification.
\newblock In {\em Proc.\ 3rd Workshop on Theory and Applications of Abstract
  Data Types}, volume 116 of {\em Informatik-Fachberichte}, pages 31--38.
  Springer, 1985.

\bibitem[ST86]{SannellaDT:eml-institution-independent86}
Donald Sannella and Andrzej Tarlecki.
\newblock Extended {ML}: An institution-independent framework for formal
  program development.
\newblock In {\em Proc.\ Workshop on Category Theory and Computer Programming},
  volume 240 of {\em Lecture Notes in Computer Science}, pages 364--389.
  Springer, 1986.

\bibitem[ST87a]{SannellaDT:observational-equivalence87}
Donald Sannella and Andrzej Tarlecki.
\newblock On observational equivalence and algebraic specification.
\newblock {\em Journal of Computer and System Sciences}, 34:150--178, 1987.

\bibitem[ST87b]{SannellaDT:implementations-revisited87}
Donald Sannella and Andrzej Tarlecki.
\newblock Toward formal development of programs from algebraic specifications:
  Implementations revisited.
\newblock In {\em Proc.\ 12th Colloq.\ on Trees in Algebra and Programming.
  Intl.\ Joint Conf.\ on Theory and Practice of Software Development
  ({TAPSOFT}'87)}, volume 249 of {\em Lecture Notes in Computer Science}, pages
  96--110. Springer, 1987.
\newblock \textbf{Extended abstract; the final full version of this is
  \cite{SannellaDT:implementations-revisited88}}.

\bibitem[ST88a]{SannellaDT:WADT88}
Donald Sannella and Andrzej Tarlecki.
\newblock {\em Recent Trends in Data Type Specification: 5th Workshop on
  Specification of Abstract Data Types --- Selected Papers}, volume 332 of {\em
  Lecture Notes in Computer Science}.
\newblock Springer, 1988.

\bibitem[ST88b]{SannellaDT:specs-arbitrary-institution88}
Donald Sannella and Andrzej Tarlecki.
\newblock Specifications in an arbitrary institution.
\newblock {\em Information and Computation}, 76:165--210, 1988.

\bibitem[ST88c]{SannellaDT:lfcs-newsletter-tools88}
Donald Sannella and Andrzej Tarlecki.
\newblock Tools for formal program development: Some fantasies.
\newblock {\em {LFCS} Newsletter}, 1:10--15, 1988.

\bibitem[ST88d]{SannellaDT:implementations-revisited88}
Donald Sannella and Andrzej Tarlecki.
\newblock Toward formal development of programs from algebraic specifications:
  Implementations revisited.
\newblock {\em Acta Informatica}, 25:233--281, 1988.

\bibitem[ST89]{SannellaDT:eml-methodology89}
Donald Sannella and Andrzej Tarlecki.
\newblock Toward formal development of {ML} programs: Foundations and
  methodology.
\newblock In {\em Proc.\ Colloq.\ on Current Issues in Programming Languages.
  Intl.\ Joint Conf.\ on Theory and Practice of Software Development
  ({TAPSOFT}'89)}, volume 352 of {\em Lecture Notes in Computer Science}, pages
  375--389. Springer, 1989.

\bibitem[ST91a]{SannellaDT:eml-overview91}
Donald Sannella and Andrzej Tarlecki.
\newblock {E}xtended {ML}: Past, present and future.
\newblock In {\em Proc.\ 7th Workshop on Specification of Abstract Data Types},
  volume 534 of {\em Lecture Notes in Computer Science}, pages 297--322.
  Springer, 1991.

\bibitem[ST91b]{SannellaDT:asl+91}
Donald Sannella and Andrzej Tarlecki.
\newblock A kernel specification formalism with higher-order parameterisation.
\newblock In {\em Proc.\ 7th Workshop on Specification of Abstract Data Types},
  volume 534 of {\em Lecture Notes in Computer Science}, pages 274--296.
  Springer, 1991.

\bibitem[ST92]{SannellaDT:model-theoretic-foundations92}
Donald Sannella and Andrzej Tarlecki.
\newblock Toward formal development of programs from algebraic specifications:
  Model-theoretic foundations.
\newblock In {\em Proc.\ 19th Intl.\ Colloq.\ on Automata, Languages and
  Programming}, volume 623 of {\em Lecture Notes in Computer Science}, pages
  656--671. Springer, 1992.
\newblock \textbf{This is superceded by
  \cite{SannellaDT:essential-concepts97}}.

\bibitem[ST93]{SannellaDT:real-problems93}
Donald Sannella and Andrzej Tarlecki.
\newblock Algebraic specification and formal methods for program development:
  What are the real problems?
\newblock In G.~Rozenberg and A.~Salomaa, editors, {\em Current Trends in
  Theoretical Computer Science. Essays and Tutorials}, pages 115--120. World
  Scientific, 1993.
\newblock Originally published in \emph{EATCS Bulletin} 41:134--137 (1990).

\bibitem[ST96]{SannellaDT:mind-the-gap96}
Donald Sannella and Andrzej Tarlecki.
\newblock Mind the gap! {A}bstract versus concrete models of specifications.
\newblock In {\em Proc.\ 21st Intl.\ Symp.\ on Mathematical Foundations of
  Computer Science}, volume 1113 of {\em Lecture Notes in Computer Science},
  pages 114--134. Springer, 1996.

\bibitem[ST97]{SannellaDT:essential-concepts97}
Donald Sannella and Andrzej Tarlecki.
\newblock Essential concepts of algebraic specification and program
  development.
\newblock {\em Formal Aspects of Computing}, 9:229--269, 1997.

\bibitem[ST99a]{SannellaDT:alg-methods99}
Donald Sannella and Andrzej Tarlecki.
\newblock Algebraic methods for specification and formal development of
  programs.
\newblock {\em ACM Computing Surveys}, 31(3es), 1999.

\bibitem[ST99b]{SannellaDT:prelimaries96}
Donald Sannella and Andrzej Tarlecki.
\newblock Algebraic preliminaries.
\newblock In Egidio Astesiano, Hans-J{\"o}rg Kreowski, and Bernd
  Krieg-Br{\"u}ckner, editors, {\em Algebraic Foundations of Systems
  Specification}, chapter~2. Springer, 1999.

\bibitem[ST03]{SannellaDT:foundations03}
Donald Sannella and Andrzej Tarlecki.
\newblock Foundations.
\newblock In {\em {CASL} User Manual}, volume 2900 of {\em Lecture Notes in
  Computer Science}, chapter~10, pages 125--129. Springer, 2003.

\bibitem[ST04]{SannellaDT:CASL-semantics04}
Donald Sannella and Andrzej {Tarlecki, editors}.
\newblock {CASL} semantics.
\newblock In Peter Mosses, editor, {\em {CASL} Reference Manual}, volume 2960
  of {\em Lecture Notes in Computer Science}, pages 115--274. Springer, 2004.

\bibitem[ST06]{SannellaDT:horizontal-composition06}
Donald Sannella and Andrzej Tarlecki.
\newblock Horizontal composability revisited.
\newblock In {\em Algebra, Meaning and Computation: Essays Dedicated to Joseph
  A. Goguen on the Occasion of his 65th Birthday}, volume 4060 of {\em Lecture
  Notes in Computer Science}, pages 296--316. Springer, 2006.

\bibitem[ST08]{SannellaDT:observability08}
Donald Sannella and Andrzej Tarlecki.
\newblock Observability concepts in abstract data type specification, 30 years
  later.
\newblock In {\em Concurrency, Graphs and Models: Essays Dedicated to Ugo
  Montanari on the Occasion of his 65th Birthday}, Lecture Notes in Computer
  Science. Springer, 2008.

\bibitem[ST12]{SannellaDT:FASFSD12}
Donald Sannella and Andrzej Tarlecki.
\newblock {\em Foundations of Algebraic Specification and Formal Software
  Development}.
\newblock EATCS Monographs in Theoretical Computer Science. Springer, 2012.

\bibitem[ST14]{SannellaDT:prop-oriented-sem13}
Donald Sannella and Andrzej Tarlecki.
\newblock Property-oriented semantics of structured specifications.
\newblock {\em Mathematical Structures in Computer Science}, 24(2):e240205, 37
  pages, 2014.

\bibitem[ST15]{SannellaDT:asl-legacy15}
Donald Sannella and Andrzej Tarlecki.
\newblock The foundational legacy of {ASL}.
\newblock In {\em Software, Services and Systems: Essays Dedicated to Martin
  Wirsing on the Occasion of His Emeritation}, volume 8950 of {\em Lecture
  Notes in Computer Science}, pages 253--272. Springer, 2015.

\bibitem[SW82]{SannellaDT:implementations82}
Donald Sannella and Martin Wirsing.
\newblock Implementation of parameterised specifications.
\newblock In {\em Proc.\ 9th Intl.\ Colloq.\ on Automata, Languages and
  Programming}, volume 140 of {\em Lecture Notes in Computer Science}, pages
  473--488. Springer, 1982.

\bibitem[SW83]{SannellaDT:asl83}
Donald Sannella and Martin Wirsing.
\newblock A kernel language for algebraic specification and implementation.
\newblock In {\em Proc.\ 1983 Intl.\ Conf.\ on Foundations of Computation
  Theory}, volume 158 of {\em Lecture Notes in Computer Science}, pages
  413--427. Springer, 1983.

\bibitem[SW87]{SannellaDT:modular-prolog87}
Donald Sannella and Lincoln Wallen.
\newblock A calculus for the construction of modular {P}rolog programs.
\newblock In {\em Proc.\ 1987 {IEEE} Symp.\ on Logic Programming}, pages
  368--378, 1987.
\newblock \textbf{Extended abstract; the final full version of this is
  \cite{SannellaDT:modular-prolog92}}.

\bibitem[SW92]{SannellaDT:modular-prolog92}
Donald Sannella and Lincoln Wallen.
\newblock A calculus for the construction of modular {P}rolog programs.
\newblock {\em Journal of Logic Programming}, 12:147--177, 1992.

\bibitem[SW99]{SannellaDT:specification-languages96}
Donald Sannella and Martin Wirsing.
\newblock Specification languages.
\newblock In Egidio Astesiano, Hans-J{\"o}rg Kreowski, and Bernd
  Krieg-Br{\"u}ckner, editors, {\em Algebraic Foundations of Systems
  Specification}, chapter~8. Springer, 1999.

\bibitem[WS87]{SannellaDT:functional-programming-intro87}
Martin Wirsing and Donald Sannella.
\newblock Une introduction {\`a} la programmation fontionnelle: {HOPE} et {ML}.
\newblock {\em Technique et Science Informatiques}, 6:517--525, 1987.

\end{thebibliography}