By the same authors

Kleene Algebra in Unifying Theories of Programming

Research output: Working paper

Standard

Kleene Algebra in Unifying Theories of Programming. / Foster, Simon David.

2018.

Research output: Working paper

Harvard

Foster, SD 2018 'Kleene Algebra in Unifying Theories of Programming'.

APA

Foster, S. D. (2018). Kleene Algebra in Unifying Theories of Programming.

Vancouver

Foster SD. Kleene Algebra in Unifying Theories of Programming. 2018 Apr 5.

Author

Foster, Simon David. / Kleene Algebra in Unifying Theories of Programming. 2018.

Bibtex - Download

@techreport{4221361ccd7849acafe6971ba345a3ac,
title = "Kleene Algebra in Unifying Theories of Programming",
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.",
author = "Foster, {Simon David}",
year = "2018",
month = "4",
day = "5",
language = "English",
type = "WorkingPaper",

}

RIS (suitable for import to EndNote) - Download

TY - UNPB

T1 - Kleene Algebra in Unifying Theories of Programming

AU - Foster, Simon David

PY - 2018/4/5

Y1 - 2018/4/5

N2 - 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.

AB - 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.

M3 - Working paper

BT - Kleene Algebra in Unifying Theories of Programming

ER -