Mechanising a Unifying Theory

DOI10.1007/11768173_13MaRDI QIDQ5307484zbMATH OpenOpenAlexFDO

Authors Gift Nuka, Jim Woodcock

Publication date 14 September 2007

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

Full work available at URL https://doi.org/10.1007/11768173_13

Mathematics Subject Classification ID

General topics in the theory of software (68N01)

Recommendations

• Unifying theories in ProofPower-Z
• Mechanical reasoning about families of UTP theories
• Isabelle/UTP: a mechanised theory engineering framework
• Unifying Theories in ProofPower-Z
• Mechanical Reasoning about Families of UTP Theories

Cited in

(15)

• A UTP semantics for \textsf{Circus}
• Unifying theories in ProofPower-Z
• Angelic nondeterminism and unifying theories of programming
• A stepwise approach to linking theories
• An Axiomatic Value Model for Isabelle/UTP
• UTPCalc -- a calculator for UTP predicates
• Unifying heterogeneous state-spaces with lenses
• Higher-order UTP for a theory of methods
• Mechanical reasoning about families of UTP theories
• scientific article; zbMATH DE number 1140687 (Why is no real title available?)
• Mechanical Reasoning about Families of UTP Theories
• Retrospective and Prospective for Unifying Theories of Programming
• Unifying Theories in ProofPower-Z
• On the existence of universally convergent mechanisms
• On the existence of universally convergent mechanisms

Describes a project that uses

Uses Software

• HOL
• ProofPower
• Z
• EVES

This page was built for publication: Mechanising a Unifying Theory

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