Reference Manual

The reference manual tries to document the current status of CafeOBJ. It is generated from the in-system help.

PDF VersionHTML Version.

The reference manual is also available as Wiki on Github.

User Manual

A slightly outdated manual targeting new users, which introduces many of the concepts of CafeOBJ in more details.

PDF Version

PTcalc Manual

This manual describes the PTcalc commands for automatic proof search.

PDF Version

Other documents


Brief Introduction to CafeOBJ by Takahiro Seino in English and Japanese.

For further tutorial, please see the dedicated section Tutorials.


  • CafeOBJ Report
    The Language, Proof Techniques, and Methodologies for Object-Oriented Algebraic Specification
    Amast Series in Computing, Vol.6, World Scientific, 1998
    by Razen Diaconescu and Kokichi Futatsugi
  • Other publication can be found at the respective members pages.