Kleene Algebra in Unifying Theories of Programming

Simon David Foster

Kleene Algebra in Unifying Theories of Programming

Computer Science

Research output: Working paper

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.

Original language	English
Number of pages	6
Publication status	Unpublished - 5 Apr 2018

Access to Document

UTP-KAT

Southwest University, Chongqing
Jim Woodcock (Advisor) & Zhiming Liu (Collaborator)
11 May 2019 → 15 May 2019
Activity: Visiting an external institution › Academic

Cite this

@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 = apr,

day = "5",

language = "English",

type = "WorkingPaper",

}

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 -

Kleene Algebra in Unifying Theories of Programming

Abstract

Access to Document

Activities

Southwest University, Chongqing

Cite this