CafeOBJ for Real -- Using an algebraic specification language as theorem prover
講師：Norbert Preining
担当：MathLibre Project
レベル：入門編
対象者：関数型言語，定理自動証明，代数型言語に興味を持っている方
前提知識：プログラミング言語について基礎的な知識を有する方
※本セミナーは、日本語での講演です
CafeOBJ is a many- and order-sorted algebraic specification language
from the Obj family, related to languages like Casl and Maude. CafeOBJ
allows us to have both the specification and the verification in the
same language. It is based on powerful logical foundations
(order-sorted algebra, hidden algebra, and rewriting logic) with an
executable semantics. It has been used to specify and verify extensive
systems (e.g., railway signal systems, e-commerce protocols,
authentication protocols), but at the same time it functions equally
well as theorem prover using the built-in rewrite engine.
On the other hand, provable properties of computations on reals are
highly desirable, and computational models of the reals based on sound
logical foundations with effective algorithm form a favorable
approach. Computational models of the reals are wide, ranging from
interval arithmetic to all kind of sequence approximations, in
particular streams (signed digit streams etc). Representing streams in
a formal framework requires extra caution, as streams are infinite
objects. Typical approaches use coinductive definitions.
Stream processing is a specific case of behavioral rewrite systems,
and thus can be implemented in CafeOBJ, which provides hidden sorts
allowing us to specify infinite data objects via a behavioral,
i.e. coinductive, approach.
In this talk we will cover the following two topics:
(*) Short introduction to CafeOBJ, in particular its syntax, its
formal background in institutions.
(*) practical programming examples from the functional programming world,
(*) implementation of modules for the representation of exact reals,
with some usage examples.
【カテゴリ】プログラミング言語
