Projects / OBJ3


OBJ3 is a program specification and proof system based on order sorted equational logic. It has been successfully used for research and teaching in software design and specification, rapid prototyping, theorem proving, user interface design, and hardware verification, among other things. It was the first language to implement parameterized programming and its module system influenced the designs of the Ada, C++, and ML module systems.

Operating Systems

Recent releases

  •  08 Apr 2005 02:41

    Release Notes: This version now compiles completely and will load and run in several Common Lisp implementations. OBJ3 is now supported in GNU Common Lisp, Steel Bank Common Lisp, CMU Common Lisp, and OpenMCL on GNU/Linux on the x86 platform and Mac OS X on PowerPC.

    •  29 Sep 2003 16:47

      Release Notes: This release has been updated to recent versions of GCL (2.5.3), CMU Common Lisp (18e), glibc (2.3), and gcc (3.2), and provides a pre-built executable for a mainstream modern Linux distribution (Red Hat 8.0).

      •  03 Dec 2001 02:57

        Release Notes: Inclusion of Lutz Hamel's TRIM compilation system (which helps some specifications interpret ten times faster), build tests with GCL 2.4.0 and GCL 2.3, a build test with GCC 3.0.1, and new documentation for TRIM inclusion.

        •  07 Jul 2000 18:37

          Release Notes: First Freshmeat announcement.


          Project Spotlight


          A Fluent OpenStack client API for Java.


          Project Spotlight

          TurnKey TWiki Appliance

          A TWiki appliance that is easy to use and lightweight.