By the same authors

Kleene Algebra in Unifying Theories of Programming

Research output: Working paper

Full text download(s)

Author(s)

Department/unit(s)

Publication details

DateUnpublished - 5 Apr 2018
Number of pages6
Original languageEnglish

Abstract

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.

Activities

Discover related content

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

View graph of relations