By the same authors

An Axiomatic Value Model for Isabelle/UTP

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

Full text download(s)

Author(s)

Department/unit(s)

Publication details

Title of host publication6th International Symposium on Unifying Theories of Programming
DateAccepted/In press - 2016
Pages1-20
Number of pages20
Original languageEnglish

Abstract

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.

Discover related content

Find related publications, people, projects, datasets and more using interactive charts.

View graph of relations