Wolfram Kahl
pp. 178-190 in
Rudolf Berghammer, Bernhard Möller, Georg Struth (ed.)
Relational and {Kleene}-Algebraic Methods in Computer Science: {7th International Seminar on Relational Methods in Computer Science and 2nd International Workshop on Applications of Kleene Algebra, Bad Malente, Germany, May 12--17, 2003, Revised Selected Papers,
LNCS
3051, Springer-Verlag, 2003.
(.bib)
We propose a collection of theories in the proof assistant Isabelle/Isar that support calculational reasoning in and about heterogeneous relational algebras and Kleene algebras.