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 papers:
Maintained by Joseph Goguen
To the research projects index page
Last modified: Thu Jun 17 21:40:10 PDT 2004