A modular coding of \textsc{Unity} in \textsc{Coq}

DOI10.1007/BFB0105409MaRDI QIDQ6567718zbMATH OpenFDO

Authors Barbara Heyd, P. Crégut

Publication date 5 July 2024

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

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• Logical foundations for compositional verification and development of concurrent programs in UNITY
• On the logic of UNITY
• Mechanizing UNITY in Isabelle
• On mechanizing proofs within a complete proof system for Unity
• scientific article; zbMATH DE number 2077135

Cites work

• Eliminating the substitution axiom from UNITY logic
• Extensions of the UNITY methodology: compositionality, fairness and probability in parallelism
• The calculus of constructions
• The formal specification and design of a distributed electronic funds-transfer system

This page was built for publication: A modular coding of \textsc{Unity} in \textsc{Coq}

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