Paper Info
Title
Unifying Theories of Programming in Isabelle
Abstract
This is a tutorial introduction to the two most basic theories in Hoare & He's Unifying Theories of Programming and their mechanisation in the Isabelle interactive theorem prover. We describe the theories of relations and of designs pre-postcondition pairs, interspersed with their formalisation in Isabelle and example mechanised proofs.
Year
DOI
Venue
2013
10.1007/978-3-642-39721-9_3
ICTAC Training School on Software Engineering
Keywords
Field
DocType
isabelle,laws of programming,denotational semantics,unifying theories of programming utp,interactive theorem proving
Programming language,Computer science,Denotational semantics,Algorithm,Theoretical computer science,Mathematical proof,Proof assistant
Conference
Citations 
PageRank 
References 
6
0.50
27
Authors
2
Name
Order
Citations
PageRank
Simon Foster16313.44
Jim Woodcock253477.08