Alasdair Armstrong, Simon Foster, Georg Struth, and Tjark Weber. Archive of Formal Proofs, January 2014. Formal proof development.
Tarski's algebra of binary relations is formalised along the lines of the standard textbooks of Maddux and Schmidt and Ströhlein. This includes relation-algebraic concepts such as subidentities, vectors and a domain operation as well as various notions associated to functions. Relation algebras are also expanded by a reflexive transitive closure operation, and they are linked with Kleene algebras and models of binary relations and Boolean matrices.
The original publication is available at http://afp.sf.net/entries/Relation_Algebra.shtml.
@article{armstrong13kleene,
author = {Alasdair Armstrong and Simon Foster and Georg Struth and Tjark Weber},
title = {Relation Algebra},
journal = {Archive of Formal Proofs},
month = jan,
year = {2014},
note = {\url{http://afp.sf.net/entries/Relation_Algebra.shtml}, Formal proof development}
}