Welcome to the CafeOBJ official homepage!
|Location||Home page URL|
CafeOBJ is a new generation algebraic specification and programming language. As a direct successor of OBJ, it inherits all its features(flexible mix-fix syntax, powerful typing system with sub-types, and sophisticated module composition system featuring various kinds of imports, parameterised modules, views for instantiating the parameters, module expressions, etc.) but it also implements new paradigms such as rewriting logic and hidden algebra, as well as their combination.
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.
The execution of CafeOBJ in compiled mode is based on a rewriting machine that gives CafeOBJ the same efficiency as modern functional programming systems.
The Cafe environment supports distributed interactive proofs over Internet and specification methodologies in CafeOBJ.