Isabelle/UTP: Mechanised Theory Engineering for Unifying Theories of Programming (Q7361736)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry UTP
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Isabelle/UTP: Mechanised Theory Engineering for Unifying Theories of Programming |
AFP entry UTP |
Statements
1 February 2019
0 references
Simon Foster
0 references
Frank Zeyda
0 references
Yakoub Nemouchi
0 references
Pedro Ribeiro
0 references
Burkhart Wolff
0 references
Isabelle/UTP: Mechanised Theory Engineering for Unifying Theories of Programming (English)
0 references
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.
0 references
0 references
