Isabelle/UTP swMATH ID: 21184 Software Authors: Foster, Simon; Zeyda, Frank; Woodcock, Jim Description: 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. Homepage: https://www-users.cs.york.ac.uk/~simonf/utp-isabelle/ Dependencies: Isabelle/HOL Related Software: Circus; Z; Isabelle/HOL; Archive Formal Proofs; Sledgehammer; Isabelle; ProofPower; Isabelle/Circus; UTP2; HOL; Lifting; Transfer; Handel-C; seL4; UTPCalc; PVS; Coq; Saoithin; ArcAngel; TLA Cited in: 17 Publications Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year Isabelle/UTP: a mechanised theory engineering framework. Zbl 1457.68061Foster, Simon; Zeyda, Frank; Woodcock, Jim 2015 all top 5 Cited by 27 Authors 9 Foster, Simon 8 Woodcock, James C. P. 6 Cavalcanti, Ana 4 Zeyda, Frank 2 Gleirscher, Mario 2 Ribeiro, Pedro 1 Amálio, Nuno 1 Baxter, James 1 Bowen, Jonathan P. 1 Butterfield, Andrew 1 Calinescu, Radu C. 1 Canham, Samuel 1 Colvin, Robert J. 1 Freitas, Leo 1 Hayes, Ian J. 1 He, Jifeng 1 Huerta y Munive, Jonathan Julián 1 Kelly, Tim 1 Meinicke, Larissa A. 1 Nemouchi, Yakoub 1 Sheng, Feng 1 Struth, Georg 1 Thiele, Bernhard 1 Wei, Ran 1 Yang, Zongyuan 1 Ye, Kangfeng 1 Zhu, Huibiao Cited in 3 Serials 4 Formal Aspects of Computing 2 Theoretical Computer Science 1 Journal of Logical and Algebraic Methods in Programming Cited in 2 Fields 17 Computer science (68-XX) 1 Systems theory; control (93-XX) Citations by Year