Mechanizing bisimulation theorems for relation-changing logics in Coq

DOI10.1007/978-3-030-38808-9_1MaRDI QIDQ777873zbMATH OpenOpenAlexFDO

Authors Raul Fervari, Francisco Trucco, Beta Ziliani

Publication date 8 July 2020

Full work available at URL https://doi.org/10.1007/978-3-030-38808-9_1

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Mechanization of proofs and logical operations (03B35)

Recommendations

• Verification of dynamic bisimulation theorems in Coq
• Formalizing cut elimination of coalgebraic logics in Coq
• Mechanizing common knowledge logic using COQ
• Relation-changing modal operators
• Relation-changing logics as fragments of hybrid logics

Cited in

(2)

• Coalgebraic Reasoning in Coq: Bisimulation and the λ-Coiteration Scheme
• Verification of dynamic bisimulation theorems in Coq

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Mechanizing bisimulation theorems for relation-changing logics in Coq

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