Isabelle/UTP

An Isabelle-based proof environment for UTP

Isabelle/UTP is an embedding of Hoare and He's Unifying Theories of Programming in Isabelle/HOL. The UTP is a semantic framework for the formalisation, comparison, and integration of a variety of a computational paradigms, with the aim of providing a comprehensive approach to formal semantics. Our embedding in Isabelle, though essentially deep, integrates with Isabelle/HOL type checking and proof tactics, thus providing a powerful platform for UTP proof.

This work is partly supported by EU FP7 Project COMPASS (grant agreement 287829).

Comprehensive Modelling for Advanced Systems of Systems