|
Isabelle/UTP:
Mechanised
Theory
Engineering
for
Unifying
Theories
of
Programming
Title: |
Isabelle/UTP: Mechanised Theory Engineering for Unifying Theories of Programming |
Authors:
|
Simon Foster,
Frank Zeyda,
Yakoub Nemouchi (yakoub /dot/ nemouchi /at/ york /dot/ ac /dot/ uk),
Pedro Ribeiro and
Burkhart Wolff
|
Submission date: |
2019-02-01 |
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. |
BibTeX: |
@article{UTP-AFP,
author = {Simon Foster and Frank Zeyda and Yakoub Nemouchi and Pedro Ribeiro and Burkhart Wolff},
title = {Isabelle/UTP: Mechanised Theory Engineering for Unifying Theories of Programming},
journal = {Archive of Formal Proofs},
month = feb,
year = 2019,
note = {\url{http://isa-afp.org/entries/UTP.html},
Formal proof development},
ISSN = {2150-914x},
}
|
License: |
BSD License |
Status: [ok] |
This is a development version of this entry. It might change over time
and is not stable. Please refer to release versions for citations.
|
|