Kleene Algebra in Unifying Theories of Programming

Research output: Working paper


This development links Isabelle/UTP to the mechanised Kleene Algebra (KA) hiearchy for Isabelle/HOL. We substantiate the required KA laws, and provides a large body of additional theorems for alphabetised relations which are provided by the KA library. Additionally, we show how such theorems can be lifted to a subclass of UTP theories, provided certain conditions hold.
Original languageEnglish
Number of pages6
Publication statusUnpublished - 5 Apr 2018

Cite this