Verification of dynamic bisimulation theorems in Coq

DOI10.1016/j.jlamp.2021.100642OpenAlexW3126024677MaRDI QIDQ2035655

Raul Fervari, Beta Ziliani, Francisco Trucco

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

bisimulationmodal logicsdynamic logicsproof mechanization

Mathematics Subject Classification ID

Computer science (68-XX)

Related Items (1)

To be announced

Uses Software

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

Cites Work

• Mechanizing bisimulation theorems for relation-changing logics in Coq
• Isabelle. A generic theorem prover
• Dynamic epistemic logics of introspection
• Introspection as an action in relational models
• Axiomatising logics with separating conjunction and modalities
• Mechanizing focused linear logic in Coq
• Logics of public communications
• Hybrid logics: characterization, interpolation and complexity
• Reactive Kripke Semantics
• Moving Arrows and Four Model Checking Results
• THE EXPRESSIVE POWER OF MEMORY LOGICS
• ARROW UPDATE LOGIC
• The Lean Theorem Prover (System Description)
• Expressive Power and Decidability for Memory Logics
• A Brief Overview of HOL4
• Dynamic Epistemic Logic and Knowledge Puzzles
• Dynamic logic of preference upgrade
• Separation logics and modalities: a survey
• Modal logics of sabotage revisited
• Relation-changing modal operators: Fig. 1.
• Global and Local Graph Modifiers
• Swap logic
• FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science
• The power of modal separation logics
• Axiomatic and dual systems for constructive necessity, a formally verified equivalence
• A FORMAL PROOF OF THE KEPLER CONJECTURE
• Introducing Reactive Kripke Semantics and Arc Accessibility
• Mechanizing Mathematical Reasoning
• Semantical Analysis of Modal Logic I Normal Modal Propositional Calculi
• Verified Decision Procedures for Modal Logics.
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

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