Toggle Main Menu Toggle Search

Open Access padlockePrints

An Axiomatic Value Model for Isabelle/UTP

Lookup NU author(s): Dr Leo Freitas

Downloads


Licence

This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License (CC BY-NC 4.0).


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 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 approaches. We carefully craft a definitional mechanism in the Isabelle/HOL prover that guarantees soundness.


Publication metadata

Author(s): Zeyda F, Foster S, Freitas L

Editor(s): Jonathan Bowen and Huibiao Zhu

Publication type: Conference Proceedings (inc. Abstract)

Publication status: Published

Conference Name: 6th International Symposium on Unifying Theories of Programming (UTP 2016)

Year of Conference: 2016

Print publication date: 23/06/2016

Acceptance date: 17/04/2016

Date deposited: 13/05/2016

URL: http://utp2016.ecnu.edu.cn


Share