Lecturer
Norbert Preining
JAIST, Research Center for Software Verification, Japan
Place/Time
日本数式処理学会 第２４回大会 (24. Annual Meeting of the Japan Society for Symbolic and Algebraic Computation)
2015-06-16, Tsukuba University, Tsukuba, 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 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.