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.

• 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 examples.
   
• 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 logic integration.
   
• [New] Scritical Pairs and Sunification, with Monica Marcus, to appear in 18th 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 available.
   
• [New] 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 the web.
   
• 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 postscript).
   
• 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.