- SCIA is an interactive but highly automated
tool for data integration; it is being used in the large NSF SEEK (Science Environment for
Ecological Research) project, for generating mappings between data sets
having different schemas of different kinds, and for matching ports in
- Griot is a system for live
genraeting interactive multimedia events; its homepage has links to
documentation of performances that used it.
- Alloy is an algorithm for blending
conceptual spaces; it is used in Griot
to generate novel metaphors on the fly, for use in live interactive
- BOBJ is a behavioral specification
and verification system based on hidden
algebra and the syntax of OBJ3; the BOBJ homepage has many examples showing the
surprising power of circular coinductive rewriting, and illustrating other
novel features, such as higher order modules, case analysis, concurrent
connection, and cobasis declaration. BOBJ is written in pure Java, and you
can get the most recent version from the BOBJ ftp site.
- Kumo is a proof assistant for
first order logic with atoms from equational logic and hidden algebra, that automatically generates
websites that document its proofs; there are many proof websites you can browse. The most
recent version of Kumo can be downloaded from the Kumo ftp site. Kumo is
part of the Tatami project.
version 2.06 is an open source release of OBJ3, evolved from version 2.04, 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 OBJ family homepage describes several
versions and extensions of OBJ, including CafeObj, Maude,
and of course OBJ3 and BOBJ; there are also links to many examples
and to detailed documentation.
- FOOPS, a declarative object oriented language
built on top of OBJ3.
- TOOR, a requirements management system built on
top of FOOPS.
- Eqlog, a logic programming language, implemented
by enriching OBJ3 with order sorted unification
- TRIM, an optimizing compiler for OBJ, specified
and proved correct using OBJ3.
- OOZE, an object oriented version of Z built on
top of FOOPS.
- 2OBJ, a theorem prover (for any user definable
logic) built using OBJ3.
Maintained by Joseph Goguen
Last modified: Sun Jan 1 11:26:20 PST 2006