An Axiomatic Value Model for Isabelle/UTP

DOI10.1007/978-3-319-52228-9_8MaRDI QIDQ2971180zbMATH OpenOpenAlexFDO

Authors Frank Zeyda, Simon Foster, Leo Freitas

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

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

Recommendations

• Isabelle/UTP: a mechanised theory engineering framework
• Axiom schemes for m-valued propositions calculi
• Towards a UTP semantics for Modelica
• scientific article; zbMATH DE number 3877155
• scientific article; zbMATH DE number 1231562
• ON THE AXIOMATIZATION OF FINITE-VALUED LOGICAL CALCULI
• Modular bisimulation theory for computations and values
• Formalizing axiomatic systems for propositional logic in Isabelle/HOL
• scientific article; zbMATH DE number 2185692
• A constructive valuation semantics for classical logic

Cites work

• A consistent foundation for Isabelle/HOL
• A process algebraic framework for specification and validation of real-time systems
• A UTP semantics for \textsf{Circus}
• Edinburgh LCF. A mechanized logic of computation
• Extending Sledgehammer with SMT solvers
• Formalising foundations of mathematics
• Foundational, compositional (co)datatypes for higher-order logic: category theory applied to theorem proving
• Higher-order UTP for a theory of methods
• Isabelle/HOL. A proof assistant for higher-order logic
• Isabelle/UTP: a mechanised theory engineering framework
• Mechanical reasoning about families of UTP theories
• Mechanising a Unifying Theory
• Object-Orientation in the UTP
• Partizan Games in Isabelle/HOLZF
• Saoithín: a theorem prover for UTP
• The consistency theorem for free type definitions in \(Z\)
• The logic of \(U\cdot(TP)^{2}\)
• The safety-critical Java memory model formalised
• Unifying theories in Isabelle/HOL
• Unifying theories in ProofPower-Z

Cited in

(12)

• Towards verification of cyber-physical systems with UTP and Isabelle/HOL
• Unifying theories of reactive design contracts
• Isabelle/UTP: a mechanised theory engineering framework
• A stepwise approach to linking theories
• Unifying theories in Isabelle/HOL
• Unifying heterogeneous state-spaces with lenses
• Mechanical reasoning about families of UTP theories
• UTP, \textsf{\textit{Circus}}, and Isabelle
• Optics
• Shallow Expressions
• Isabelle/UTP: Mechanised Theory Engineering for Unifying Theories of Programming
• Z Mathematical Toolkit in Isabelle/HOL

Describes a project that uses

Uses Software

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

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2971180)