A Coq implementation of the program algebra in Jifeng He's new roadmap for linking theories of programming

DOI10.1007/978-3-031-40436-8_15MaRDI QIDQ6535845zbMATH OpenFDO

Authors Rundong Mu, Qin Li

Publication date 28 February 2024

zbMATH Keywords

refinementCoqprogram algebraunifying theories of programming

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• A new roadmap for linking theories of programming
• Linking theories of probabilistic programming
• Kleene algebra with tests and Coq tools for while programs
• Algebras for program correctness in Isabelle/HOL
• Theorem-proving support in programming language semantics

Cites work

• scientific article; zbMATH DE number 1949583 (Why is no real title available?)
• scientific article; zbMATH DE number 7178362 (Why is no real title available?)
• A denotational semantics of simulink with higher-order UTP
• Approximate bisimulation and discretization of hybrid CSP
• Denotational semantics and its algebraic derivation for an event-driven system-level language
• Denotational semantics of channel mobility in UTP-CSP
• Hybrid relations in Isabelle/UTP
• Isabelle/UTP: a mechanised theory engineering framework
• Laws of programming
• Refinement-oriented probability for CSP
• Translation of CCS into CSP, correct up to strong bisimulation
• Unifying Theories in ProofPower-Z
• Unifying theories in Isabelle/HOL

This page was built for publication: A Coq implementation of the program algebra in Jifeng He's new roadmap for linking theories of programming

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