Mechanizing UNITY in Isabelle

DOI10.1145/343369.343370MaRDI QIDQ5738896zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Lawrence C. Paulson

Publication date 13 June 2017

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/343369.343370

zbMATH Keywords

compositional reasoningconcurrencyIsabelleUNITY

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• A mechanization of unity in PC-NQTHM-92
• Mechanizing compositional reasoning for concurrent systems: some lessons
• scientific article; zbMATH DE number 2077135
• On the logic of UNITY
• Unifying theories of programming in Isabelle

Cited in

(10)

• An experiment concerning mathematical proofs on computers with French undergraduate students
• A mechanization of unity in PC-NQTHM-92
• Specification and verification of concurrent programs through refinements
• Mechanizing compositional reasoning for concurrent systems: some lessons
• Liveness properties in CafeOBJ -- a case study for meta-level specifications
• A Formalized Theory for Verifying Stability and Convergence of Automata in PVS
• Reflection principles for synthetic theories of smooth manifolds
• On mechanizing proofs within a complete proof system for Unity
• A modular coding of \textsc{Unity} in \textsc{Coq}
• Cones and foci: A mechanical framework for protocol verification

Describes a project that uses

Uses Software

• Isabelle
• HOL-UNITY
• HOL
• Coq
• UNITY

This page was built for publication: Mechanizing UNITY in Isabelle

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