An Axiomatic Value Model for Isabelle/UTP

Frank Zeyda; Simon David Foster; Leo Freitas

An Axiomatic Value Model for Isabelle/UTP

Frank Zeyda, Simon David Foster, Leo Freitas

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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.

Original language	English
Title of host publication	6th International Symposium on Unifying Theories of Programming
Pages	1-20
Number of pages	20
Publication status	Accepted/In press - 2016
Event	6th International Symposium on Unifying Theories of Programming - Reykjavík, Iceland Duration: 4 Jun 2016 → 5 Jun 2016

Conference

Conference	6th International Symposium on Unifying Theories of Programming
Country/Territory	Iceland
City	Reykjavík
Period	4/06/16 → 5/06/16

Access to Document

paper_8Accepted author manuscript, 375 KB

Cite this

@inproceedings{36eb03fdbcce48fab1e02c3d4ecb71b1,

title = "An Axiomatic Value Model for Isabelle/UTP",

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.",

author = "Frank Zeyda and Foster, {Simon David} and Leo Freitas",

year = "2016",

language = "English",

pages = "1--20",

booktitle = "6th International Symposium on Unifying Theories of Programming",

note = "6th International Symposium on Unifying Theories of Programming ; Conference date: 04-06-2016 Through 05-06-2016",

}

TY - GEN

T1 - An Axiomatic Value Model for Isabelle/UTP

AU - Zeyda, Frank

AU - Foster, Simon David

AU - Freitas, Leo

PY - 2016

Y1 - 2016

N2 - 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.

AB - 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.

M3 - Conference contribution

SP - 1

EP - 20

BT - 6th International Symposium on Unifying Theories of Programming

T2 - 6th International Symposium on Unifying Theories of Programming

Y2 - 4 June 2016 through 5 June 2016

ER -