Semantics of Computation
As computers extend their reach into our lives, with new applications,
increased connectivity, and ever increasing power, it becomes ever more
important to understand what they are doing, and to be sure that it is what
we want them to be doing. This in turn requires more abstract descriptions
of what they should be doing, and more powerful ways of verifying that they
are doing it, i.e., it requires more abstract specification techniques and
more powerful theorem proving methods, which in particular, must be able to
handle behavioral properties of concurrent distributed systems. Other
important issues include modularization of larger systems, and using
multi-perspective specification, based on multiple languages.
The first three items below provide a good place to acquire background
needed to read the other material; the next two items give computer science
oriented introductions to aspects of category theory. An up to date listing
of all recent papers is given on my What's New
page. See also my course CSE 230, Principles of
Programming Languages, on the principles that underlie the various kinds
of programming language, which includes some introductory material on
algebraic semantics, and also the proof
displays generated by the Kumo proof
assistant and website generator, including coinductive proofs.
The following is a roughly inverse chronological list of other relevant
- Algebraic Semantics of Imperative Programs,
by Joseph Goguen and Grant
Malcolm (MIT Press, 1996). ISBN 0-262-07172-X. Covers most features of
imperative languages using algebraic semantics; many exercises that can be
done using OBJ3; also contains entry level introductions to universal algebra
and OBJ3. [The paper An Executable Course
in the Algebraic Semantics of Imperative Programs discusses some
pedagogical innovations of this book.]
- Two chapters from Theorem proving and
Algebra, by Joseph Goguen, to be published by MIT Press, someday; an
introduction to both general algebra and theorem proving. Chapter 1, the Introduction and Chapter 8, on First Order Logic, plus the References and the Table of
Contents are available. Chapter 8 (finished 15 September 1998) gives an
elegant algebraic exposition of first order logic, proof planning and
induction; the treatment of induction is unusually general, and there are many
- Software Engineering with OBJ: algebraic specification in action,
edited by Joseph Goguen and Grant
Malcolm, Kluwer, 2000; ISBN 0-7923-7757-5. A book on OBJ and its
applications. The Introduction and
the papers Introducing OBJ and More Higher Order Programming with OBJ3,
are available; Introducing OBJ is
essentially a user manual for OBJ3.
- A Categorical Manifesto, by Joseph
Goguen, in Mathematical Structures in Computer Science, Volume 1,
Number 1, March 1991, pages 49-67.
- What is Unification?, by Joseph
Goguen, in Resolution of Equations in Algebraic Structures, Volume 1:
Algebraic Techniques, edited by Maurice Nivat and Hassan Ait-Kaci,
Academic Press, 1989, pages 217-261.
- [New] Extended abstract of Data, Schema and Ontology Integration, for
the Lisbon CombLog'04
Workshop, 28-30 July 2004. A pdf
version is also available. Motivation and theory for a "data integration
chain," from data to schema to ontology to ontology language to ontology
Scritical Pairs and Sunification, with Monica Marcus, to appear in
Wrokshop on Unification (Cork, Ireland, 4-5 July 2004); new methods
for proving confluence based on generalizations of critical pairs and
unification. A pdf version is also
Verification with Proof Scores in CafeOBJ, by Kokichi Futatsugi,
Joseph Goguen, and Kazuhiro Ogata. In Abstracts of Presentations at
Workshop on Algebraic Development Techniques, ed. Peter Mosses, 2004,
pages 75-78 (Barcelona, 27-29 March). A short description of a semi-formal
approach to software verification.
- Composing Hidden Information Modules over
Inclusive Institutions, by Joseph Goguen and Grigore Rosu. Semantics for specification
combining operations that can hide information; necessary and sufficient
conditions for using only visible consequences of hidden information to be
safe; applications to programming language module systems. To appear in
From Object-Orientation to Formal Methods: Essays in Memory of Ole-Johan
Dahl, Springer Lecture Notes in Computer Science, vol. 2635, edited by
Olaf Owe, Stein Krogdahl and Tom Lyche.
- Behavioral Verification of Distributed
Concurrent Systems with BOBJ, by Joseph Goguen and Kai Lin. Text of
keynote lecture for Conference on
Quality Software, Dallas TX, 5-6 November 2003. In Proceedings,
Conference on Quality Software, IEEE Press 2003, pages 216-235. Some slides are also available, although they are
much more technical than the talk that was actually given. The paper proves
correctness of the alternating bit protocol making strong use of recent
features of BOBJ, especially conditional
circular coinductive rewriting with case analysis. An early version of this
paper is A Hidden Proof of the Alternating Bit
Protocol, by Kai Lin and Joseph Goguen. See also the brief early
web note Correctness of the
Alternating Bit Protocol, and proof sketch for the Petersen Critical Section Algorithm.
- Conditional Circular Coinductive Rewriting
with Case Analysis, by Joseph Goguen, Kai Lin and Grigore Rosu, in Recent Trends in
Algebraic Development Techniques, Springer Lecture Notes in Computer
Science, volume 2755, 2004, pages 216-232; proceedings of 16th Workshop on
Algebraic Development Techniques, Frauenchiemsee, Germany, 24-27
September 2002. Slides for the lecture version are also available, Conditional Circular Coinductive Rewriting
(Note: You may have to reorient to "seascape"), as is the two page abstract,
Conditional Circular Coinductive
Rewriting, by the same authors. This paper extends BOBJ's circular
coinductive rewriting algorithm to conditional equations and "splits" for
case analyses. Note: This version does not have proofs.
- Morphisms and Semantics for Higher Order
Parameterized Programming, by Kai Lin and Joseph Goguen, a paper on
higher order parameterized modules, generalizing views to morphisms, and
giving a semantics based on functors from slice categories. An abstract is available for this paper, as are a pdf version of the paper and a pdf version of the abstract.
- An Induction Scheme in Higher
Order Parameterized Programming, by Joseph Goguen and Kai Lin. A
"programming pearl" using induction schema to illustrate higher order modules
and higher order views in BOBJ.
- Institution Morphisms, by
Joseph Goguen and Grigore Rosu, in
Formal Aspects of Computing 13, 2002, pages 274-307; special issue
edited by Don Sannella, in honor of the retirement of Rod Burstall. This
paper brings greater order to the chaotic menagerie of different genres and
species of morphisms between institutions, by exploring their basic
properties and some important relationships among them, and by giving them
systematic suggestive names.
- A Hidden Herbrand Theorem: Combining the
Object, Logic and Functional Paradigms, by Joseph Goguen, Grant Malcolm, and Tom Kemp,
Journal of Logic and Algebraic Programming, Volume 51, 2002, pages
1-41. Shows how to combine the logic and object paradigms using hidden
algebra with existential quantifiers. This is a journal version of a paper
in Principles of Declarative Programming, edited by Catuscia
Palamidessi, Hugh Glaser and Karl Meinke (Proceedings of PLIP/ALP'98
[Programming Languages, Implementations, Logics and Programs / Algebraic and
Logic Programming], Pisa, Italy, 14-19 September 1998), Springer Lecture
Notes in Computer Science, Volume 1490, pages 445-462. (The paper was
completed in 2001, and uses an older version of hidden algebra.) A pdf version is also available.
- Circular Coinduction by Grigore Rosu and Joseph Goguen, in
Proceedings, International Joint Conference on Automated Deduction,
Sienna, June 2001. This paper provides the full proof of correctness of
circular coinduction, and draws some consequences, including various
congruence criteria. A gzipped postscript
version is also available.
- Hidden Coinduction, by Joseph
Goguen and Grant Malcolm, in
Mathematical Structures in Computer Science, 9, number 3, pages
287-319, June 1999.
- A Hidden Agenda, by Joseph Goguen and
Grant Malcolm, Theoretical
Computer Science, , vol 245, no 1, pages 55-101, August 2000; special
issue on Algebraic Engineering, edited by Chrystopher Nehaniv and Masami Ito.
This is a basic paper on hidden algebra, treating coinduction, nondeterminism,
concurrency and more. A compressed postscript
version is also available. An earlier version is UCSD Technical Report CS97-538, April 1997, and an
obsolete abstract is in Proceedings of Workshop on New Mathematics
for Computer Science, in Conference on Intelligent Systems: A Semiotic
Perspective (National Institute of Standards and Technology, Gaithersberg MD,
20-23 Oct 1996) pages 159-167.
- Stretching First Order Equational Logic:
Proofs with Partiality, Subtypes and Retracts, by Joseph Goguen.
Watch retracts at work and at play! See how cute they are, and how useful
they can be for proving results about partial functions. Submitted for
publication; last modified 2 June 1998. An obsolete version is in
Proceedings, International Workshop on First Order Theorem proving
(Schloss Hagenbert, Austria, 27-28 October 1997) edited by Maria Paola
Bonacina and Ulrich Furbach, RISC-Linz Report 97-70, pages 78-85, 1997; the complete proceedings are available on
- Hidden Algebra for Software
Engineering, by Joseph Goguen, in Combinatorics, Computation and
Logic, Proceedings, Conference on Discrete Mathematics and Theoretical
Computer Science, (University of Auckland, New Zealand, 18-21 January 1999),
edited by Cristian Calude
and Michael Dinneen; Australian Computer Science Communications, Volume
21, Number 3, Springer, pages 35-59, 1999. A gentle introduction to hidden
algebra, with simple examples, much motivation, and some history.
- Parameterized Programming and Software
Architecture, by Joseph Goguen, in Proceedings, Fourth
International Conference on Software Reuse, IEEE Computer Society, April 1996,
pages 2-11 (keynote address).
- Sheaf Semantics for Concurrent Interacting
Objects, by Joseph Goguen, in Mathematical Structures in Computer
Science, Volume 2, 1992, pages 159-191.
- Logical Support for
Modularization, by Razvan Diaconescu, Joseph Goguen and Petros
Stefaneas, in Logical Environments, edited by Gerard Huet and Gordon
Plotkin, Cambridge, 1993, pages 83-130.
- Hyperprogramming: A Formal Approach to
Software Environments, by Joseph Goguen, in Proceedings,
Symposium on Formal Approaches to Software Technology, Joint System
Development Corp., Tokyo Japan, January 1990.
- Institutions: Abstract Model Theory for
Specification and Programming, by Joseph Goguen and Rod Burstall,
Journal of the Association for Computing Machinery, Volume 39, Number
1, January 1992, pages 95-146; also, Report ECS-LFCS-90-106, Department of
Computer Science, University of Edinburgh, January 1990. (Drafts of this
paper go as far back as 1985.)
- An Oxford Survey of Order Sorted
Algebra, by Joseph Goguen and Razvan Diaconescu, Mathematical
Structures in Computer Science, Volume 4, 1994, pages 363-392.
- Order-Sorted Algebra I: Equational
Deduction for Multiple Inheritance, Overloading, Exceptions and Partial
Operations, by Joseph Goguen and Jose Meseguer, Theoretical
Computer Science, volume 105, no. 2, 1992, pages 217-273 (in pure
- Types as Theories, by Joseph
Goguen, in Topology and Category Theory in Computer Science, edited by
George Michael Reed, Andrew William Roscoe and Ralph F Wachter, Oxford
University Press, 1991, pages 357-390 (in pure postscript). Proceedings of a
Conference held at Oxford, June 1989.
- Higher Order Functions Considered
Unnecessary for Higher Order Programming, by Joseph Goguen, in
Research Topics in Functional Programming, edited by David Turner,
University of Texas at Austin Year of Programming Series, Addison-Wesley,
1990, pages 309-352; also Technical Report SRI-CSL-88-1, Computer Science
Lab, SRI International, January 1988.
Maintained by Joseph Goguen
To the research projects index page
Last modified: Thu Jun 17 21:40:10 PDT 2004