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_15zbMATH Open1547.68129MaRDI QIDQ6535845FDOQ6535845

Authors: Rundong Mu, Qin Li 

Publication date: 28 February 2024

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

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)

Cites Work

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

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)