Verification of dynamic bisimulation theorems in Coq
type: Item
instance of: scholarly article
title: Verification of dynamic bisimulation theorems in Coq
author: Raul Fervari
author: Francisco Trucco
author: Beta Ziliani
published in: Journal of Logical and Algebraic Methods in Programming
publication date: 2021-06-25T00:00:00Z
Mathematics Subject Classification ID: 68-XX
zbMATH DE Number: 7363407
zbMATH Keywords: modal logics
zbMATH Keywords: dynamic logics
zbMATH Keywords: bisimulation
zbMATH Keywords: proof mechanization
describes a project that uses: kepler98
describes a project that uses: Mtac
describes a project that uses: Lean
describes a project that uses: Coq
describes a project that uses: Isabelle
describes a project that uses: HOL
MaRDI profile type: Publication
full work available at URL: j.jlamp.2021.100642
OpenAlex ID: W3126024677
cites work: Modal logic
cites work: Semantical Analysis of Modal Logic I Normal Modal Propositional Calculi
cites work: Dynamic Epistemic Logic and Knowledge Puzzles
cites work: Q3408862
cites work: Mechanizing Mathematical Reasoning
cites work: FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science
cites work: Relation-changing modal operators: Fig. 1.
cites work: Introducing Reactive Kripke Semantics and Arc Accessibility
cites work: Reactive Kripke Semantics
cites work: Global and Local Graph Modifiers
cites work: Logics of public communications
cites work: Expressive Power and Decidability for Memory Logics
cites work: THE EXPRESSIVE POWER OF MEMORY LOGICS
cites work: Hybrid logics: Characterization, interpolation and complexity
cites work: Modal logics of sabotage revisited
cites work: Moving Arrows and Four Model Checking Results
cites work: Swap logic
cites work: Q5302559
cites work: A FORMAL PROOF OF THE KEPLER CONJECTURE
cites work: A Brief Overview of HOL4
cites work: Isabelle. A generic theorem prover
cites work: Q4942002
cites work: Verified Decision Procedures for Modal Logics.
cites work: The Lean Theorem Prover (System Description)
cites work: Axiomatic and dual systems for constructive necessity, a formally verified equivalence
cites work: Mechanizing focused linear logic in Coq
cites work: Mechanizing bisimulation theorems for relation-changing logics in Coq
cites work: Q4342096
cites work: ARROW UPDATE LOGIC
cites work: Q5419882
cites work: Dynamic logic of preference upgrade
cites work: Dynamic epistemic logics of introspection
cites work: Introspection as an action in relational models
cites work: Q4525781
cites work: Separation logics and modalities: a survey
cites work: Q5224566
cites work: Axiomatising logics with separating conjunction and modalities
cites work: The power of modal separation logics
DOI: 10.1016/J.JLAMP.2021.100642
description: scientific article; zbMATH DE number 7363407