Isabelle/UTP: a mechanised theory engineering framework. We introduce Isabelle/UTP, a novel mechanisation of Hoare and He’s unifying theories of programming (UTP) in Isabelle/HOL. UTP is a framework for the study, formalisation, and unification of formal semantics. Our contributions are, firstly, a deep semantic model of UTP’s alphabetised predicates, supporting meta-logical reasoning that is parametric in the underlying notions of values and types. Secondly, integration of host-logic type checking that subsumes the need for typing proof obligations in the object-language. Thirdly, proof tactics that transfer results from well-supported mathematical structures in Isabelle to proofs about UTP theories. Additionally, our work provides novel insights towards reconciliation of shallow and deep language embeddings.
Keywords for this software
References in zbMATH (referenced in 10 articles , 1 standard article )
Showing results 1 to 10 of 10.
- Foster, Simon; Cavalcanti, Ana; Canham, Samuel; Woodcock, Jim; Zeyda, Frank: Unifying theories of reactive design contracts (2020)
- Ribeiro, Pedro; Cavalcanti, Ana: Angelic processes for CSP via the UTP (2019)
- Butterfield, Andrew: Utpcalc -- a calculator for UTP predicates (2017)
- Colvin, Robert J.; Hayes, Ian J.; Meinicke, Larissa A.: Designing a semantic model for a wide-spectrum language with concurrency (2017)
- Foster, Simon; Thiele, Bernhard; Cavalcanti, Ana; Woodcock, Jim: Towards a UTP semantics for Modelica (2017)
- Ribeiro, Pedro; Cavalcanti, Ana; Woodcock, Jim: A stepwise approach to linking theories (2017)
- Zeyda, Frank; Foster, Simon; Freitas, Leo: An axiomatic value model for Isabelle/UTP (2017)
- Cavalcanti, Ana; Woodcock, Jim; Amálio, Nuno: Behavioural models for FMI co-simulations (2016)
- Foster, Simon; Zeyda, Frank; Woodcock, Jim: Unifying heterogeneous state-spaces with lenses (2016)
- Foster, Simon; Zeyda, Frank; Woodcock, Jim: Isabelle/UTP: a mechanised theory engineering framework (2015)