Verification of dynamic bisimulation theorems in Coq

DOI10.1016/J.JLAMP.2021.100642MaRDI QIDQ2035655zbMATH OpenOpenAlexFDO

Authors Raul Fervari, Francisco Trucco, Beta Ziliani

Publication date 25 June 2021

Published in Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.jlamp.2021.100642

zbMATH Keywords

bisimulationdynamic logicsmodal logicsproof mechanization

Mathematics Subject Classification ID

Computer science (68-XX)

Recommendations

• Mechanizing bisimulation theorems for relation-changing logics in Coq
• Formalizing cut elimination of coalgebraic logics in Coq
• The impact of including model update operators in modal logics
• A natural deduction approach to dynamic logic
• scientific article; zbMATH DE number 4047196

Cites work

• A Brief Overview of HOL4
• A formal proof of the Kepler conjecture
• Arrow update logic
• Axiomatic and dual systems for constructive necessity, a formally verified equivalence
• Axiomatising logics with separating conjunction and modalities
• Dynamic Epistemic Logic and Knowledge Puzzles
• Dynamic epistemic logics of introspection
• Dynamic logic of preference upgrade
• Expressive Power and Decidability for Memory Logics
• Formal proof - the four color theorem
• FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science
• General dynamic dynamic logic
• Global and local graph modifiers
• Handbook of modal logic
• scientific article; zbMATH DE number 1028833 (Why is no real title available?)
• scientific article; zbMATH DE number 1556014 (Why is no real title available?)
• scientific article; zbMATH DE number 1418447 (Why is no real title available?)
• Hybrid logics: Characterization, interpolation and complexity
• Introducing Reactive Kripke Semantics and Arc Accessibility
• Introspection as an action in relational models
• Isabelle. A generic theorem prover
• Logics of public communications
• Mechanizing bisimulation theorems for relation-changing logics in Coq
• Mechanizing focused linear logic in Coq
• Mechanizing Mathematical Reasoning
• Modal logic
• Modal logics of sabotage revisited
• Moving Arrows and Four Model Checking Results
• On the complexity of modal separation logics
• Reactive Kripke semantics
• Relation-changing modal operators
• Semantical Analysis of Modal Logic I Normal Modal Propositional Calculi
• Separation logics and modalities: a survey
• Swap logic
• The expressive power of memory logics
• The Lean theorem prover (system description)
• The power of modal separation logics
• Verified Decision Procedures for Modal Logics.

Cited in

(6)

• scientific article; zbMATH DE number 4022620 (Why is no real title available?)
• scientific article; zbMATH DE number 1301729 (Why is no real title available?)
• To be announced
• Graded relation updates in modal logic
• Mechanizing bisimulation theorems for relation-changing logics in Coq
• Tilting at windmills with Coq: Formal verification of a compilation algorithm for parallel moves

Describes a project that uses

Uses Software

• kepler98
• Mtac
• Lean
• Coq
• Isabelle
• HOL

This page was built for publication: Verification of dynamic bisimulation theorems in Coq

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