Logical Foundations of CafeOBJ (abstract)

This paper surveys the logical foundations and semantics of CafeOBJ, which is a successor of the famous algebraic specification language OBJ but adding several new primitive paradigms such as rewriting logic and behavioural concurrent specification.

We first give a concise overview of CafeOBJ. Then we concentrate on the actual logical foundations of the language. We survey some novel or more classical theoretical concepts supporting the logical semantics of CafeOBJ together with pointing to the main results but without giving proofs and without discussing all mathematical details. However for proofs and for some of the mathematical details not discussed here we give pointers to relevant publications.

The logical foundations of CafeOBJ are structured by the concept of institution. Moreover, the design of CafeOBJ emerged from its

logical foundations, and institution concepts played a crucial role in structuring the language design.

---