CafeOBJ is a most advanced formal specification language which inherits many advanced features (e.g. flexible mix-fix syntax,powerful and clear typing system with ordered sorts, parameteric modules and views for instantiating the parameters, and module expressions, etc.) from OBJ (or more exactly OBJ3) algebraic specification language.

CafeOBJ is a language for writing formal (i.e. mathematical) specifications of models for wide varieties of software and systems, and verifying properties of them. CafeOBJ implements equational logic by rewriting and can be used as a powerful interactive theorem proving system. Specifiers can write proof scores also in CafeOBJ and doing proofs by executing the proof scores.

CafeOBJ has state-of-art rigorous logical semantics based on institutions. The CafeOBJ cube shows the structure of the various logics underlying the combination of the various paradigms implemented by the language. Proof scores in CafeOBJ are also based on institution based rigorous semantics, and can be constructed using a complete set of proof rules.


  • Specification and Verification with Proof Scores in CafeOBJ - Lecturer FUTATSUGI, Kokichi JAIST, Research Center for Software Verification, Japan Place/Time 2015-10-23 and 10-30, NII, Tokyo, Japan. Web site Please see this page for details. Abstract CafeOBJ is a most advanced algebraic formal specification language system with rewriting/reduction engine which can be used for interactive verification. Proof scores are scripts for verifications and provide versatile […]
  • CafeOBJ course at the ESSLLI 2016 - The European Summer School in Logic, Language and Information ESSLLI is a yearly event that normally brings together several hundred students and teachers for two weeks of courses. Next year’s ESSLLI 2016 will be held in Bozen, Italy. One of the courses will be Algebraic Specification and Verification – an Introduction to CafeOBJ by Kokichi […]
  • CafeOBJ 1.5.4 released - We have released a new version of CafeOBJ, which incorporates besides other fixes the following changes: CITP changes new commands :ctf- and :csp- new command :def(ine) to turn :ctf(-) and :csp(-) into proper tactics for :apply new tactics nf, ct improvements in the online help system bug fixes in AC rewriting small changes in the […]
  • Algebraic specifications and Functional programming with CafeOBJ - Lecturer Norbert Preining JAIST, Research Center for Software Verification, Japan Place/Time Mathematical Software and Free Documents XXI 2015-09-12, Kyoto, Japan. Abstract CafeOBJ is an algebraic specification language based on equational order-sorted logic, which incorporates rewriting logic and hidden algebras. What sets it apart from other specification languages is that it is also executable, means that […]
  • Getting CafeOBJ via MacPorts - I have finally finished the Portfile for CafeOBJ, which allows users to install CafeOBJ via the usual port command of MacPorts. For one needs to add our local source (which only ships CafeOBJ port), but I hope to get the port into the standard distribution soon. Necessary steps: Add the following line to your MacPorts […]