Description
Applications
Download
Related papers
Documentation
  . tactics
  . modules
  . dependencies
Notes
Authors Acknowledgements

Damien Pous' home page

Relation Algebra and KAT in Coq

This Coq development is a modular library about relation algebra: those algebras admitting heterogeneous binary relations as a model, ranging from partially ordered monoid to residuated Kleene allegories and Kleene algebra with tests (KAT).

This library presents this large family of algebraic theories in a modular way; it includes several high-level reflexive tactics:

  • kat, which decides the (in)equational theory of KAT;
  • hkat, which decides the Hoare (in)equational theory of KAT (i.e., KAT with Hoare hypotheses);
  • ka, which decides the (in)equational theory of KA;
  • ra, a normalisation based partial decision procedure for Relation algebra;
  • ra_normalise, the underlying normalisation tactic.
  the cloud of relation algebra fragments

The tactic for Kleene algebra with tests is obtained by reflection, using a simple bisimulation-based algorithm working on the appropriate automaton of partial derivatives, for the generalised regular expressions corresponding to KAT. Combined with a formalisation of KA completeness, and then of KAT completeness on top of it, this provides entirely axiom-free decision procedures for all models of these theories (including relations, languages, traces, min-max and max-plus algebras, etc...).

Algebraic structures are generalised in a categorical way: composition is typed like in categories, allowing us to reach "heterogeneous" models like rectangular matrices or heterogeneous binary relations, where most operations are partial. We exploit untyping theorems to avoid polluting decision algorithms with these additional typing constraints.

Applications

We give a few examples of applications of this library to program verification:

Download

This library is available through opam, under the name coq-relation-algebra, as well as on GitHub.

Related papers or talks

Documentation

Provided tactics

Succinct description of each module

Each module is documented; links below point to the coqdoc generated documentation; see below for dependencies. The coqdoc table of contents is here.

Modules dependencies

Notes

This library started by a complete rewrite of the ATBR library we developed with Thomas Braibant. There was two main reasons for not reusing this code:

Authors

Acknowledgements

I am grateful to Thomas Braibant, with whom we developed the ancestor of this library, clearing the ground for this subsequent work.



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