In their Unifying Theories of Programming (UTP), Hoare & He use the alphabetised relational calculus to give denotational semantics to a wide variety of constructs taken from different programming paradigms.
UTP is the basis for the semantics of the languages in the Circus family of notations.
In this page, we describe work developed at York that is specific to UTP, and also provide links to download the UTP book.
Isabelle/UTP is an implementation of UTP in the theorem prover Isabelle/HOL.
Department of Computer Science
Deramore Lane, University of York, Heslington, York, YO10 5GH, UK
Tel: 01904 325500 | Fax: 01904 325599
