What's New on this site -
and What's Cool on the web
The Tatami Project
LINKS for a Hidden World -- using Kumo and BOBJ
("LINKS" could be an acronym for something like "Library Information
Network Knowledge System".)
The Tatami system supports distributed cooperative design,
specification and validation of (software and/or hardware) systems,
especially distributed concurrent systems. The Tatami system integrates
formal with informal methods, has an online tutorial capability, runs over
the web, and is intended to be useful to ordinary software engineers. The
underlying formal logic is first order logic with atoms from hidden (order sorted) algebra. User
interface design has been guided by algebraic semiotics and narratology, which are
respectively the theories of signs and of stories.
Note: "Tatami" are natural fiber mats used in
traditional Japanese buildings. The size of a room is measured by the number
of tatami on its floor, where each tatami is a rectangle about 5 by 3 feet.
Thus a 2 tatami room, like a 2 tatami proof, is pretty small, an 8 tatami room
(or proof) is ok, but a 12 tatami room (or proof) is getting large, and should
probably be subdivided. Tatami are cool, refreshing and aromatic; we hope you
will find this metaphor helpful when creating and browsing proofs.
The figure above suggests how the Tatami system works; some components
are clickable for further detail. The main components are the Kumo proof assistant and website generator ("kumo" is a
Japanese word for spider), the tatami protocol,
the barista generic proof server, the tatami database,
the BOBJ behavioral specification language, and one or
more proof engines, each with a server (the current implementation uses a
slightly old version of BOBJ). Kumo assists multiple distributed users with
design and validation, and automatically generates websites to document their
work. Kumo reads commands written in the Duck
language, reads specifications in the BOBJ language,
checks proofs using proof engines, and then generates "proofweb" data
structures in XML, which are then translated into HTML for proof
documentation, based on the tatami conventions.
Information is broadcast to other sites using the tatami protocol, and all local tatami databases
(including truth values) are updated locally. Any standard web browser can
be used to view the websites generated by Kumo, and to execute the proof
scores on remote proof engines via barista servers.
We do not aspire to mechanize proofs like those of which mathematicians are
justly so proud, but rather to provide support that is useful to practicing
engineers for design, specification and validation. We also do not aspire to
build powerful theorem provers to compete with existing provers like HOL,
Nqthm, PVS and Otter; instead, we intend to re-use them.
For more detail, see Web-based
Support for Cooperative Software Engineering, by Joseph Goguen and Kai Lin,
in Annals of Software Engineering, volume 12, 2001; a pdf version is also available. See also
the brief summary of results as of Sept. 2001, the
brief report by Prof. Rod Burstall, and the one page
progress summary for our NSF grant up to October 1999, Hidden Algebra and Concurrent Distributed
Software, which appeared in Software Engineering Notes. A
description of the previous Tatami system design appears in An Overview of the Tatami Project,
which appeared in Cafe: An Industrial-Strength Algebraic Formal
Method, edited by Kokichi Futatsugi, Tetsuo Tamai and Ataru Nakagawa,
Elsevier, 2000, pages 61-78. Many further details are given in papers listed
A number of websites generated by Kumo have been organized to form a
tutorial on our approach and some of its underlying technologies, including
website generation, website design principles, proof by reduction, first order
proof planning, hidden algebra (especially coinduction), interactive browsing,
executing proof scores on remote proof servers, interactive Java applets
illustrating key concepts of specifications and verifications, web-based
tutorials on first order logic and hidden algebra, and explanation web pages
for specs and major proof steps. (Of course, many proofs do not admit a
picture or applet to illustrate the main ideas, or even of the result.) These
websites were all generated completely automatically by Kumo, of course using
files supplied by the user for specifications, explanations and goals. The
use of Kumo guarantees that these proofs are completely formally correct. The
Kumo demos homepage gives further information about
Kumo and these examples:
The first example proves a simple formula about natural numbers,
illustrating the use of simple first order logic and induction. The second
example proves a simple property of a very simple software object, a flag, and
illustrates some basic concepts of hidden algebra, including behavioral
properties and coinduction. The third example proves the correctness of
implementing a stack with a pointer and an array; this is more complex than
the previous example, and uses more sophisticated coinduction techniques for
refinement. The first and fourth examples use induction, but the fourth is
considerably more complex, since it involves several inductive lemmas. The
fifth example has a different flavor, because it uses operations with multiple
hidden arguments. The seventh is a proof by contradiction, making heavy use
of first order logic; it is quite different from other examples, and
demonstrates the power of Kumo as a proof assistant.
- An inductive proof that 1+...+ n = n(n+1) /
2. This will give you a chance to explore Kumo's navigation and
display conventions on a simple example.
- A coinductive proof of a behavioral property of
a simple flag object. This illustrates some basics of hidden algebra on a
very simple example, including an especially clear explanation of the need for
- Two proofwebs for some familiar inductive properties of lists. The first
was generated by a duck score written at the beginning of this effort; it is
striking that the lemmas needed to complete the proof can be deduced from the
way that successive proof attempts fail. The second proofweb succeeds, and
was generated by a duck score derived from the first just by reordering its
goals so that the lemmas that were found necessary are proved first.
- This early attempt at proving that the
reverse of the reverse of a list is the original list, takes a direct
approach, and its explanations emphasize the way that the two lemmas that are
needed to complete the proof can be deduced from the output produced by
unsuccessful proof attempts; one of these lemmas is the associativity of
- Here are the complete proofs for all three
inductive properties of lists, including the two lemmas that are needed to
establish the main goal.
- A coinductive proof of the behavioral
correctness of the array-with-pointer implementation of stack. This
behavioral refinement proof requires introducing a non-trivial lemma, which
can also be inferred from a prior proof attempt that fails without it.
- A behavioral refinement proof of the correctness
of implementing sets with lists, using attribute coinduction.
- A simple inductive proof of a formula for the sum of the squares of the first n natural numbers. This example is deliberately very
spare, and in particular has no explanations, in order to illustrate the
default conventions that Kumo uses when a user supplies only the absolute
- A detailed proof that the square root
of 2 is irrational, illustrating the first order capabilities of Kumo.
Note that this uses and proves many auxiliary lemmas; see the directory listing. Note that no explanations have as
yet been provided for this proof or its parts.
For those who are interested in earlier stages of our research, we built a
number of demo websites by hand, in order to explore the underlying principles
and technologies. See the handmade demos homepage,
which contains the following:
One noticable difference from the new Kumo generated proofs is that they
lack a status window popup; however, this will eventually be added; the new
Kumo websites also have better format and other features. The fourth example
is a compiler correctness proof that uses both induction and coinduction, with
complex specifications and many lemmas; this industrial scale example also
illustrates how proofs that are partly informal can be supported.
- An inductive proof that 1+...+ n = n(n+1)
- A coinductive proof of a behavioral property
of a simple flag object.
- A coinductive proof of correctness of
implementing stack by pointer and array.
- A large compiler correctness proof using
both induction and coinduction, with a complex specification and many lemmas.
An intermediate stage between the examples produced by the current Kumo
system and the hand made examples, is represented by the examples in the old Kumo demos homepage:
We believe that the newer Kumo user interface is better, and in addition,
we have taken advantage of improved logical capabilites in Kumo in the proofs
in the new Kumo demos homepage.
- An inductive proof that 1+...+ n = n(n+1) /
- A coinductive proof of a behavioral property of a
simple flag object.
- A proof of behavioral correctness of the
array-with-pointer implementation of stack, using coinduction.
- An inductive proof that the reverse of the
reverse of a list is the list, with some lemmas, including that append is associative.
- A behavioral refinement proof of the correctness of
implementing sets with lists, using attribute coinduction.
- A first order logic proof that the
square root of 2 is irrational.
- An inductive proof of a formula for the sum of
the squares of the first n natural numbers.
- A coinductive correctness proof for the tatami
protocol, which maintains the consistency of distributed cooperative
proofs that are built using the Tatami system.
This project is supported by the National Science Foundation, and was
previously supported by the CafeOBJ Project at JAIST (Japan Advanced Institute of Science
and Technology), organized by Prof. Kokichi Futatsugi of JAIST.
See also the UCSD CafeOBJ
homepage and the IPA (Japan) homepage.
Other participants in the CafeOBJ project included: Mitsubishi Research
Institute, NEC, SRA and Unisys in Japan; SRI International in Menlo Park,
California; the Technical University of Munich in Germany; and the University
of Paris at Orsay.
- Joseph Goguen, Professor of Computer
Science & Engineering, UCSD. Project leader.
- Kai Lin, PhD Student, UCSD. Implementing the
- Grigore Rosu, PhD in 2001
from UCSD; now at NASA, Ames Research Center, Mountain View CA. Working on
the theory of hidden algebra and algorithms for implementing it, theory of
institutions, modal logic, etc.
Alumni and close friends of the project include:
- Prof. Rod Burstall,
University of Edinburgh, UK, 10 - 30 November 2000.
- Tashimi Sawada, SRI, Tokyo, Japan, November 1999.
- Prof. Virgil Emil
Cazanescu, University of Bucharest, Romania, June-July 1999, August 2000.
- Prof Cristian Calude,
University of Auckland, January 1999.
Padawitz, University of Dortmund, part of sabbatical, February 1998.
- Prof. Kokichi Futatsugi, of
JAIST (Japan), the Japan Advanced
Institute of Science and Technology. Head of the Language Design Lab at
- Akira Mori, Visiting Scholar (from
Kyoto University), from August 96 to June 98. Work on the library and the
tatami protocol. Now at Japan Advanced Institute for Science and Technology.
- Akiyoshi Sato, Industrial Visitor
from NEC, from March 97 to March 98. Work on the tatami protocol.
- Almira Karabeg, University of Oslo,
- Razvan Diaconescu, at JAIST and
Romanian Acad. of Sciences, Bucharest; collaborator on hidden algebra and
short term visitor.
- Eric Livingston, Visiting Scholar (from University of New England,
Armidale, Australia), from 1 Feb to 30 June 97. Sociologist; ethnomethodology
of mathematics (and other things, including checkers and chemistry).
- Bogdan Warinschi, PhD UCSD, 2004.
The use of web technologies to display designs and validations of software
systems is novel, as is the use of algebraic semiotics for interface design; see Social and Semiotic Analyses for
Theorem Prover User Interface Design for details of how designs for
the status window were improved by using semiotic morphisms. Examples in the
library range from simple illustrations of basic techniques to large scale
validations of real running systems, so that the novice can gradually become
more expert. The formal proofs use hidden algebra and various kinds of coinduction, which are believed easier to
apply than more traditional approaches like process algebra and transition
systems, because they exploit algebraic laws about methods and attributes
that are not available in these methods. The BOBJ
language is used both for specifications and as a proof engine, to dispose of
the boring details of proofs. BOBJ is a behavioral extension of the
specification aspect of OBJ3.
The following material related to this project is available:
number 1-2, 2002, pages 1-41. Shows how to combine the logic and object
paradigms using hidden algebra with existential quantifiers, giving rise to a
new programming paradigm (though it uses an older version of hidden algebra).
This is a journal version, completed in 2001, 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.
- Behavioral Verification of
Distributed Concurrent Systems with BOBJ, by Joseph Goguen and Kai
Lin. 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. 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. Some slides are also available, although they
are much more technical than the talk that was actually given. 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, edited
by Martin Wirsing, Dirk Pattinson and Rolf Hennicker, 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. This paper extends BOBJ's circular coinductive rewriting
algorithm to conditional equations and "splits" for case analyses. 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. Note: This
version does not have proofs.
- Semiotic Morphisms,
Representations, and Blending for User Interface Design, by Joseph
Goguen. Keynote lecture, in Proceedings, AMAST Workshop on
Algebraic Methods in Language Processing, AMAST Press, 2003, pages
1-15 (held Verona, Italy, 25 - 27 August 2003). This paper extends algebraic
semiotics to handle interaction by using hidden algebra; some examples are
given in detail. A pdf version of
the paper, and the slides for
the talk are also available (you may have to change the orientation to swap
- Web-based Support for
Cooperative Software Engineering, by Joseph Goguen and Kai Lin,
in Volume 12, 2001, of the Annals of Software Engineering, a special
issue on multimedia software engineering, edited by Jeffrey Tsai. This is an
overview of the Tatami project and version 4 of the Kumo website generator
and proof assistant, focusing on its design decisions, its use of multimedia
web capabilities, and its integration of formal and informal methods for
software development in a distributed cooperative environment. The paper is
a revised and expanded version of the paper Web-based Multimedia Support for
Distributed Cooperative Software Engineering, by Joseph Goguen and Kai Lin,
which appeared in Proceedings, International Symposium on Multimedia
Software Engineering, edited by Jeffrey Tsai and Po-Jen Chuang, IEEE
Press, pages 25-32; the meeting was held in Taipai, Taiwan, December 2000.
- Circular Coinductive
Rewriting by Joseph Goguen, Kai Lin, and
Grigore Rosu, in Proceedings,
Automated Software Engineering '00 (Grenoble France), September 2000,
IEEE Press, pages 123-131. Using many examples, this paper introduces the BOBJ system for behavioral specification and
computation, and its surprisingly powerful circular coinductive rewriting
algorithm for proving behavioral equalitites, which combines behavioral
rewriting with circular coinduction.
- 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 congruence criteria.
- A Hidden Herbrand Theorem:
Combining the Object, Logic and Functional Paradigms, by Joseph
Goguen, Grant Malcolm, and
Tom Kemp, in Journal of Logic and Algebraic Programming, 51
An Overview of the Tatami
Project, by Joseph Goguen, Kai Lin, Grigore Rosu, Akira Mori and
Bogdan Warinschi, in Cafe: An Industrial-Strength Algebraic Formal
Method, edited by Kokichi Futatsugi, Tetsuo Tamai and Ataru Nakagawa,
Elsevier, 2000, pages 61-78. This is a high level snapshop of the UCSD Tatami project as of late 1999. See also the one page summary
of progress on our NSF grant up to October 1999, Hidden Algebra and Concurrent Distributed
Software, in Software
Engineering Notes, volume 25, number 1, page 51, January 2000.
Behavioral and Coinductive
Rewriting, by Joseph Goguen, Kai Lin, and Grigore Rosu. Keynote address, in
Proceedings, Rewriting Logic Workshop, 2000 (Kanazawa, Japan),
edited by Kokichi Futatsugi, Japan Advanced Institute of Science and
Technology, September 2000, pages 1-22. A somewhat informal summary of
results, including simulating behavioral rewriting with standard rewriting,
and circular coinductive rewriting; the latter is a surprisingly effective
algorithm for proving behavioral equalities.
Morphisms, by Joseph Goguen. An
informal webpaper introducing some basic ideas from algebraic semiotics; for
the formal details, see An
Introduction to Algebraic Semiotics, with Applications to User Interface
Design; a pdf version is
also available. For additional information, see the author's course on user
interface design, CSE 271.
Deduction, by Grigore
Rosu and Joseph Goguen, in Automated Deduction in Classical and
Non-Classical Logics, edited by Ricardo Caferra and Gernot Salzer,
Lecture Notes in Artificial Intelligence, Volume 1761, pages 252-267, 2000.
Preliminary version in Proceedings, First-Order Theorem Proving -
FTP'98, edited by Ricardo Caferra and Gernot Salzer, Technische
Universitat Wien, pages 213-223, 1998 (proceedings of a workshop held at
Schloss Wilhelminenberg, Vienna, November 23-25, 1998). The complete proceedings are available on the
web, and by ftp. This paper
extended all the main notions and results of hidden algebra to operations
that may have more than one hidden argument, introduced the notion of
cobasis, gave criteria for operations to be congruent, and introduced more
powerful rules of deduction.
Social and Semiotic Analyses for
Theorem Prover User Interface Design, by Joseph Goguen, in Formal
Aspects of Computing, volume 11, pages 272-301, 1999. A systematic
justification of the style guidelines for the proof websites generated by Kumo, based on algebraic semiotics, narratology, cognitive
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
an early basic paper on hidden algebra, treating coinduction, nondeterminism,
concurrency and more. 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.
Slides for a lecture Towards
the Automation of Behavioral Reasoning, given by Joseph Goguen at a
meeting of IFIP WG 1.3
(Foundations of System Specification), at Stanford University on 30 June
2000; based on joint work with Kai Lin and Grigore Rosu, the slides summarize
work on hidden algebra, especially the paper Circular Coinductive Rewriting by Joseph Goguen, Kai
Lin, and Grigore Rosu.
Engineering, by Joseph Goguen, in Algebraic Engineering,
edited by Chrystopher Nehaniv and Masami Ito, World Scientific, 1999, pages
17-36; also UCSD Technical Report CS97-569, December 1997, and preliminary
version in Proceedings, Conference on Semigroups and Algebraic
Engineering, edited by Chrystopher Nehaniv (Aizu-Wakamatsu, Japan, 24-26 Mar
1997). This is a gentle introduction to the original version of hidden
algebra, with some examples and much motivation.
Hiding More of Hidden
Algebra, by Joseph Goguen and Grigore Rosu, in FM`99 - Formal
Methods, Proceedings of World Congress on Formal Methods (Toulouse,
France, August 1999), Springer Lecture Notes in Computer Science, Volume
1709, pages 1704-1709. Some new results relating information hiding to
hidden algebra, compelling examples of behavioral operations with multiple
hidden arguments, and an improved institution for hidden algebra.
A Protocol for Distributed
Cooperative Work, by Joseph Goguen
and Grigore Rosu, in
Proceedings, Workshop on Distributed Systems, Iasi, Romania, September
1999, and in Elsevier Electronic Notes in Computer Science, 28, 1999,
pages 1-22. Uses hidden algebra to prove correctness of a novel internet
broadcast protocol which supports synchronous distributed cooperative
proving; also contains a brief summary of the main definitions and results of
hidden algebra of that time.
An Introduction to Algebraic
Semiotics, with Applications to User Interface Design, by Joseph
Goguen, in Computation for Metaphor, Analogy and Agents, edited by
Chrystopher Nehaniv, Springer Lecture Notes in Artificial Intelligence, volume
1562, 1999, pages 242-291. This is the basic paper on algebraic semiotics,
with 3/2-categories, 3/2-colimits, and many examples, especially from user
interface design; completed 28 December 1998. A preliminary version appeared
in Proceedings, Conf. on Computation for Metaphor, Analogy and Agents
(Aizu-Wakamatsu, Japan, 6-10 April 1998) pages 54-79, an earlier version of
which is Semiotic Morphisms, Technical Report CS97-553, August 1997.
A now obsolete extended abstract appeared in Proceedings, Conference on
Intelligent Systems: A Semiotic Perspective, Volume II (National Institute of
Standards and Technology, Gaithersberg MD, 20-23 Oct 1996) pages 26-31.
Hidden Algebra for Software
Engineering, 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 (keynote address). A gentle introduction to
hidden algebra, with simple examples, much motivation, and some history.
Completed 8 November 1998.
Distributed Cooperative Formal
Methods Tools, by Joseph Goguen, Kai Lin, Akira Mori, Grigore Rosu
and Akiyoshi Sato. Overview of the Tatami project tools and methods,
including hidden algebra and algebraic semiotics, with examples.
Proceedings, Automated Software Engineering (Lake Tahoe NV, 3-5
Nov. 1997), IEEE, pages 55-62.
Algebraic Semiotics, ProofWebs
and Distributed Cooperative Proving, by Joseph Goguen, Akira Mori
and Kai Lin. Describes the Tatami ProofWeb data structure and the Kumo proof
assistant and website generator, plus how semiotics was used in their design.
Proceedings, User Interfaces for Theorem Provers (Sophia Antipolis,
France, 1-2 Sept 1997), pages 25-34.
Tools for Distributed
Cooperative Engineering, by Joseph Goguen, Akira Mori, Grigore Rosu
and Kai Lin. In Proceedings, CafeOBJ Symposium (Nomazu, Japan, April
1998). Describes how the Tatami system and Kumo website editor/proof
assistant integrate formal and informal methods of software development, in a
distributed cooperative environment. ProofWebs can contain scans of envelope
backs, diagrams, applets, as well as fully formal subproofs.
Hidden Coinduction, by
Joseph Goguen and Grant Malcolm, in Mathematical
Structures in Computer Science, 9, number 3, pages 287-319, June 1999.
Signs and Representations:
Semiotics for User Interface Design, by Grant Malcolm and Joseph Goguen, in
Visual Representations and Interpretations, edited by Ray Paton and
Irene Nielson, Springer Wrokshops in Computing, 1998 (proceedings of a
workshop held in Liverpool), pages 163-172. An informal introduction to
algebraic semiotics with examples, including aspects of operating systems
interfaces. Completed 30 October 1998.
Two chapters from Theorem proving and Algebra, by Joseph Goguen,
to be published by MIT Press: Chapter 1, Introduction and Chapter 8, First Order Logic, plus the
References and the Table of Contents. Chapter 8 is an elegant
algebraic exposition of first order logic, proof planning and induction; the
approach to induction is unusually general.
Visit the "world-famous" UC San Diego
Semiotic Zoo for an astonishing collection of exotic semiotic
morphisms, each an example of bad design arising through failure to preserve
some relevant structure. (Notes: (1) The zoo is still under
construction, and currently lacks explanations for some exhibits; (2)
the zoo won a "Creativity Award" from Art & Technology.)
Algebraic Semantics of
Imperative Programs, by Joseph Goguen and Grant Malcolm
(MIT Press, 1996). ISBN 0-262-07172-X. Contains entry level introductions
to universal algebra and the OBJ3 language. [The paper An Executable Course in the Algebraic
Semantics of Imperative Programs discusses some pedagogical
innovations of this book.]
CSE 230: Principles of
Programming Languages. UCSD CSE core graduate course on the
principles that underlie the various kinds of programming language; includes
some introductory material on algebraic semantics.
version 2.06 is a new OBJ release, a cleaned-up version of OBJ3 2.04
(originally from 1992), engineered by Joseph Kiniry and Sula Ma, and built and
supported by Joseph Kiniry;
it runs under GCL 2.2.2, and has modern open source documentation.
- The Behavior Homepage lists all members
of the Behavior Discussion List,
with links to their homepages whenever we could find them; this list is
intended to facilitate discussion and progress on behavioral aspects of
computer science and mathematics, including but not limited to, versions of
hidden algebra and behavioral equational logic, observational logic, and
coalgebra, as well as systems that support them, such as CafeOBJ and the Tatami
system with its Kumo theorem prover. Email Grigore Rosu to sign on to the list, or change
your email address.
- UCSD mirror site for the
CafeOBJ homepage at Japan
Advanced Institute of Science and Technology (JAIST).
- The OBJ Language Family homepage.
- CSE 271 is the basic graduate course on User Interface Design; this website
contains some information in algebraic semiotics, and a lot of background
information that is needed to appreciate why such an approach is useful.
- CSE 230: Principles of
Programming Languages, core graduate course on the principles that
underlie the various types of programming langauges; includes some
introductory material on algebraic semantics.
- Website of Razvan Diaconescu at
Institute of Mathematics of the Romanian Academy; neat stuff on the constraint
paradigm, behavioral rewriting logic, and more.
- The Maude homepage of the
Computer Science Lab at SRI. Maude incorporates most features of OBJ3,
sometimes with small syntactic changes, and adds an implementation of rewriting logic, using a powerful new
rewriting engine, and the membership equational logic generalization of order
sorted equational logic.
- Declarative group website on algebraic
semantics at Oxford, including links to Grant Malcolm, Corina Cirstea,
James Worrell, Simone Veglioni, Sula Ma, and Andrew Stevens. Note: Grant Malcolm is now at the
University of Liverpool.
- Website of
Peter Padawitz at Universitaet Dortmund, Germany; deduction and
- Website of Horst Reichel at
Dresden; neat stuff on coalgebraic semantics for the object paradigm.
- Website of Amilcar
Sernadas at Technical University of Lisbon, Portugal; applications of
institutions, object paradigm, modal logic, and more.
- Website of Bart Jacobs at
Nijmegen, the Netherlands (formerly CWI, Amsterdam); more neat stuff on
coalgebraic semantics for the object paradigm, and also for hybrid systems.
- European Common Framework
Initiative - CoFI; project to build a Common Framework for Algebraic
Specification (the language is called CASL).
Some Software Used in the Kumo System
To the UCSD Meaning and Computation Lab
To the research projects homepage
Maintained by Joseph Goguen
Largely written by May 2002; somewhat updated March 2005