CafeOBJ as symbolic and algebraic computation engine


Norbert Preining
JAIST, Research Center for Software Verification, Japan


日本数式処理学会 第24回大会 (24. Annual Meeting of the Japan Society for Symbolic and Algebraic Computation)
2015-06-16, Tsukuba University, Tsukuba, Japan.


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 specifications can be `executed’ or rewritten
to prove properties. Furthermore, its flexible mix-fix syntax, powerful module system including inheritance and parametrized modules, it has the potential to function efficiently in various circumstances, including symbolic and algebraic computations.

In this talk we give a short introduction to CafeOBJ, go through a few examples of algebra definitions, explore CafeOBJ as functional programming language, and show how CafeOBJ can be put to use in various fields of mathematics.

Leave a comment

Your email address will not be published. Required fields are marked *