Some Quick Links for this Website
The following are some quick links to homepages for each of the following
major areas of my research:
See also the Meaning and Computation Lab
homepage.
Below are links to versions of the OBJ system and some of its relatives.
- OBJ Family homepage.
- Homepage for the BOBJ system
for behavioral specification and computation. BOBJ implements many aspects
of hidden algebra, including circular
coinductive rewriting, cobases, concurrent connection, and more; this page
contains an introduction to the system, and links to a number of examples
that use it. The latest version includes a complete implementation higher
order modules and views, equational reasoning, and support for sort
constraints; it is also more user friendly, and is almost completely upward
compatible with OBJ3.
- The most recent version of BOBJ is available at the BOBJ ftp site. The BOBJ system homepage gives an introduction
to many aspects of this system for behavioral specification and computation.
- The Kumo ftp
site provides the (more or less) most recent release of version 4 of the
Kumo proof assistant and website
generator. The BOBJ download now includes the source code.
- The CafeOBJ
homepage at Japan Advanced Institute of Science and Technology (JAIST).
See also the CafeObj section of the OBJ Family homepage.
- OBJ3 version
2.06, a cleaned up version of OBJ3 2.04 (originally from 1992),
engineered by Joseph Kiniry and Sula Ma, built and supported by Joseph Kiniry; it runs under GCL
2.2.2, and has modern open source documentation.
- OBJ3, version 2.04
ftp site, with executable code for Sun 3 and later, including Sparcs, complete
source code, and a README file.
NB: It will usually be better to use
version 2.06 - see above.
- The Behavior Homepage
lists all members of the Behavior Discussion Group, with links to their
homepages whenever we could find them.
- The Behavior Discussion List is intended to facilitate 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.
Warning: The ftp download sites require host authentication, so you
probably cannot use it from a laptop over a wireless network; also, you may
need to set the username if you use a browser.
Maintained by Joseph Goguen
Last modified: Mon Nov 7 14:24:17 PST 2005