An Axiomatic Value Model for Isabelle/UTP

Frank Zeyda, Simon David Foster, Leo Freitas

Research output: Chapter in Book/Report/Conference proceedingConference contribution


The Unifying Theories of Programming (UTP) is a mathematical framework to define, examine and link program semantics for a large variety of computational paradigms. Several mechanisations of the UTP in HOL theorem provers have been developed. All of them, however, succumb to a trade off in how they encode the value model of UTP theories. A deep and unified value model via a universal (data)type incurs restrictions on permissible value types and adds complexity; a shallow value model, directly instantiating HOL types for UTP values, retains simplicity, but sacrifices expressiveness, since we lose the ability to compositionally reason about alphabets and theories. We here propose an alternative solution that axiomatises the value model and retains the advantages of both: while it supports a unified value notion, it allows us to directly inject a closed universe of HOL types into it. We carefully craft a definitional mechanism in Isabelle/HOL that guarantees soundness.
Original languageEnglish
Title of host publication6th International Symposium on Unifying Theories of Programming
Number of pages20
Publication statusAccepted/In press - 2016
Event6th International Symposium on Unifying Theories of Programming - Reykjavík, Iceland
Duration: 4 Jun 20165 Jun 2016


Conference6th International Symposium on Unifying Theories of Programming

Cite this