Loading...
Date
2012
Abstract
U (TP)2 is a theorem prover developed to support the Unifying Theories of Programming (UTP) framework. Its primary design goal was to support the higher-order logic, alphabets, equational reasoning and \programs as predicates" style that is prevalent in much of the UTP literature, from the seminal work by Hoare & He onwards. In this paper we focus on the underlying logic of the prover, emphasising those aspects that are tailored to support the style of proof so often used for UTP foundational work. These aspects include support for alphabets, type-inferencing, explicit substitution notation, and explicit meta-notation for general variable-binding lists in quanti ers. The need for these features is illustrated by a running example that develops a theory of UTP designs. We nish with a discussion of issues regarding the soundness of the proof tool, and linkages to existing \industrial strength" provers such as Isabelle, PVS or CoQ.
Supervisor
Description
peer-reviewed
Publisher
Citation
4th Unifying Theories of Programming Symposium;
Files
Loading...
Butterfield%2C%20A.pdf
Adobe PDF, 384.91 KB
Keywords
Funding code
Funding Information
Science Foundation Ireland (SFI)
Sustainable Development Goals
External Link
Type
Meetings and Proceedings
Rights
https://creativecommons.org/licenses/by-nc-sa/1.0/