Email Gateway (Aug 22 2022 at 19:07): Email Gateway (Aug 22 2022 at 19:07):From: Tobias Nipkow <nipkow@in.tum.de>
Isabelle/UTP: Mechanised Theory Engineering for Unifying Theories of Programming
Simon Foster, Frank Zeyda, Yakoub Nemouchi, Pedro Ribeiro, Burkhart Wolff
sabelle/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.
https://www.isa-afp.org/entries/UTP.html
Enjoy!
smime.p7s
Last updated: Apr 19 2024 at 08:19 UTC