By the same authors

Kleene Algebra in Unifying Theories of Programming

Research output: Working paper

Full text download(s)



Publication details

DateUnpublished - 5 Apr 2018
Number of pages6
Original languageEnglish


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.


Discover related content

Find related publications, people, projects, datasets and more using interactive charts.

View graph of relations