The Coq mailing list

[Damien Pous <Damien.Pous AT ens-lyon.fr>]

Dear all,

I'm pleased to announce the first release of RelationAlgebra, a modular Coq library for relation algebra, including a decision tactic for Kleene algebra with tests (KAT) and it's Hoare theory.

The development is entirely axiom-free ; it comes with two simple yet illustrative applications to program verification : the certification of some compiler optimisations, and straightforward proofs of program equivalence in the IMP programming language, together with an embedding of Hoare logic for partial correctness in KAT.

The library is fully documented, it is available from the following webpage :

http://perso.ens-lyon.fr/damien.pous/ra

Comments are welcome!

Best,

Damien Pous