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.

References in zbMATH (referenced in 13 articles , 1 standard article )

Showing results 1 to 13 of 13.
Sorted by year (citations)

  1. Foster, Simon; Ye, Kangfeng; Cavalcanti, Ana; Woodcock, Jim: Automated verification of reactive and concurrent programs by calculation (2021)
  2. Gleirscher, Mario; Calinescu, Radu; Woodcock, Jim: RiskStructures: a design algebra for risk-aware machines (2021)
  3. Foster, Simon; Cavalcanti, Ana; Canham, Samuel; Woodcock, Jim; Zeyda, Frank: Unifying theories of reactive design contracts (2020)
  4. Sheng, Feng; Zhu, Huibiao; He, Jifeng; Yang, Zongyuan; Bowen, Jonathan P.: Theoretical and practical approaches to the denotational semantics for MDESL based on UTP (2020)
  5. Ribeiro, Pedro; Cavalcanti, Ana: Angelic processes for CSP via the UTP (2019)
  6. Butterfield, Andrew: UTPCalc -- a calculator for UTP predicates (2017)
  7. Colvin, Robert J.; Hayes, Ian J.; Meinicke, Larissa A.: Designing a semantic model for a wide-spectrum language with concurrency (2017)
  8. Foster, Simon; Thiele, Bernhard; Cavalcanti, Ana; Woodcock, Jim: Towards a UTP semantics for Modelica (2017)
  9. Ribeiro, Pedro; Cavalcanti, Ana; Woodcock, Jim: A stepwise approach to linking theories (2017)
  10. Zeyda, Frank; Foster, Simon; Freitas, Leo: An axiomatic value model for Isabelle/UTP (2017)
  11. Cavalcanti, Ana; Woodcock, Jim; Amálio, Nuno: Behavioural models for FMI co-simulations (2016)
  12. Foster, Simon; Zeyda, Frank; Woodcock, Jim: Unifying heterogeneous state-spaces with lenses (2016)
  13. Foster, Simon; Zeyda, Frank; Woodcock, Jim: Isabelle/UTP: a mechanised theory engineering framework (2015)