CafeOBJ as symbolic and algebraic computation engine


Lecturer

Norbert Preining
JAIST, Research Center for Software Verification, Japan

Place/Time

日本数式処理学会 第24回大会 (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.

Leave a comment

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