An Axiomatic Value Model for Isabelle/UTP

DOI10.1007/978-3-319-52228-9_8zbMath1483.68093OpenAlexW2585464184MaRDI QIDQ2971180

Leo Freitas, Simon Foster, Frank Zeyda

Publication date: 4 April 2017

Published in: Unifying Theories of Programming (Search for Journal in Brave)

Full work available at URL: http://eprints.whiterose.ac.uk/105108/1/paper_8.pdf

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (2)

Unifying Heterogeneous State-Spaces with Lenses ⋮ Unifying theories of reactive design contracts

Uses Software

• Isabelle
• ML
• Isabelle/HOL
• HOL
• ProofPower
• Saoithin
• UTP2
• Sledgehammer
• Isabelle/Circus
• Isabelle/UTP

Cites Work

• Mechanical reasoning about families of UTP theories
• A process algebraic framework for specification and validation of real-time systems
• A UTP semantics for \textsf{Circus}
• Isabelle/HOL. A proof assistant for higher-order logic
• Edinburgh LCF. A mechanized logic of computation
• The consistency theorem for free type definitions in \(Z\)
• The safety-critical Java memory model formalised
• Unifying theories in ProofPower-Z
• Isabelle/UTP: A Mechanised Theory Engineering Framework
• A Consistent Foundation for Isabelle/HOL
• Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving
• Saoithín: A Theorem Prover for UTP
• Unifying Theories in Isabelle/HOL
• Formalising foundations of mathematics
• The Logic of U ·(TP)2
• Higher-Order UTP for a Theory of Methods
• Partizan Games in Isabelle/HOLZF
• Extending Sledgehammer with SMT Solvers
• Object-Orientation in the UTP
• Mechanising a Unifying Theory

This page was built for publication: An Axiomatic Value Model for Isabelle/UTP