Isabelle/UTP: Mechanised Theory Engineering for the UTP

Simon David Foster; Frank Zeyda; Yakoub Nemouchi; Pedro Fernando De Oliveira Salazar Ribeiro; Burkhart Wolff

Isabelle/UTP: Mechanised Theory Engineering for the UTP

Simon David Foster, Frank Zeyda, Yakoub Nemouchi, Pedro Fernando De Oliveira Salazar Ribeiro, Burkhart Wolff

Computer Science

Research output: Working paper

Abstract

Isabelle/UTP is a mechanised theory engineering toolkit based on Hoare and He’s Unifying Theories of Programming (UTP). UTP enables the creation of denotational, algebraic, and operational semantics for different programming languages using an alphabetised relational calculus. We provide a semantic embedding of the alphabetised relational calculus in Isabelle/HOL, including new type definitions, relational constructors, automated proof tactics, and accompanying algebraic laws. Isabelle/UTP can be used to both capture laws of programming for different languages, and put these fundamental theorems to work in the creation of associated verification tools, using calculi like Hoare logics. This document describes the relational core of the UTP in Isabelle/HOL.

Original language	English
Number of pages	162
Publication status	Unpublished - 4 Apr 2018

Access to Document

UTP

Cite this

@techreport{72f9e6363c7241be92d55843799d1548,

title = "Isabelle/UTP: Mechanised Theory Engineering for the UTP",

abstract = "Isabelle/UTP is a mechanised theory engineering toolkit based on Hoare and He{\textquoteright}s Unifying Theories of Programming (UTP). UTP enables the creation of denotational, algebraic, and operational semantics for different programming languages using an alphabetised relational calculus. We provide a semantic embedding of the alphabetised relational calculus in Isabelle/HOL, including new type definitions, relational constructors, automated proof tactics, and accompanying algebraic laws. Isabelle/UTP can be used to both capture laws of programming for different languages, and put these fundamental theorems to work in the creation of associated verification tools, using calculi like Hoare logics. This document describes the relational core of the UTP in Isabelle/HOL.",

author = "Foster, {Simon David} and Frank Zeyda and Yakoub Nemouchi and {De Oliveira Salazar Ribeiro}, {Pedro Fernando} and Burkhart Wolff",

year = "2018",

month = apr,

day = "4",

language = "English",

type = "WorkingPaper",

}

TY - UNPB

T1 - Isabelle/UTP: Mechanised Theory Engineering for the UTP

AU - Foster, Simon David

AU - Zeyda, Frank

AU - Nemouchi, Yakoub

AU - De Oliveira Salazar Ribeiro, Pedro Fernando

AU - Wolff, Burkhart

PY - 2018/4/4

Y1 - 2018/4/4

N2 - Isabelle/UTP is a mechanised theory engineering toolkit based on Hoare and He’s Unifying Theories of Programming (UTP). UTP enables the creation of denotational, algebraic, and operational semantics for different programming languages using an alphabetised relational calculus. We provide a semantic embedding of the alphabetised relational calculus in Isabelle/HOL, including new type definitions, relational constructors, automated proof tactics, and accompanying algebraic laws. Isabelle/UTP can be used to both capture laws of programming for different languages, and put these fundamental theorems to work in the creation of associated verification tools, using calculi like Hoare logics. This document describes the relational core of the UTP in Isabelle/HOL.

AB - Isabelle/UTP is a mechanised theory engineering toolkit based on Hoare and He’s Unifying Theories of Programming (UTP). UTP enables the creation of denotational, algebraic, and operational semantics for different programming languages using an alphabetised relational calculus. We provide a semantic embedding of the alphabetised relational calculus in Isabelle/HOL, including new type definitions, relational constructors, automated proof tactics, and accompanying algebraic laws. Isabelle/UTP can be used to both capture laws of programming for different languages, and put these fundamental theorems to work in the creation of associated verification tools, using calculi like Hoare logics. This document describes the relational core of the UTP in Isabelle/HOL.

M3 - Working paper

BT - Isabelle/UTP: Mechanised Theory Engineering for the UTP

ER -