swMATH ID: 21184
Software Authors: Foster, Simon; Zeyda, Frank; Woodcock, Jim
Description: Isabelle/UTP: a mechanised theory engineering framework. We introduce Isabelle/UTP, a novel mechanisation of Hoare and He’s unifying theories of programming (UTP) in Isabelle/HOL. UTP is a framework for the study, formalisation, and unification of formal semantics. Our contributions are, firstly, a deep semantic model of UTP’s alphabetised predicates, supporting meta-logical reasoning that is parametric in the underlying notions of values and types. Secondly, integration of host-logic type checking that subsumes the need for typing proof obligations in the object-language. Thirdly, proof tactics that transfer results from well-supported mathematical structures in Isabelle to proofs about UTP theories. Additionally, our work provides novel insights towards reconciliation of shallow and deep language embeddings.
Homepage: https://www-users.cs.york.ac.uk/~simonf/utp-isabelle/
Dependencies: Isabelle/HOL
Related Software: Circus; Z; Isabelle/HOL; Archive Formal Proofs; Sledgehammer; Isabelle; ProofPower; Isabelle/Circus; UTP2; HOL; Lifting; Transfer; Handel-C; seL4; UTPCalc; PVS; Coq; Saoithin; TLA; ArcAngel
Cited in: 17 Publications

Citations by Year