Formalizing the Institution for Event-B in the Coq Proof Assistant
Conor Reynolds · Lecture notes in computer science · 2021
Abstract We formalize a fragment of the theory of institutions sufficient to establish basic facts about the institution "Image missing" for Event-B, and its relationship with the institution "Image missing" for first-order predicate logic. We prove the satisfaction condition for "Image missing" and encode the institution comorphism "Image missing" embedding "Image missing" in "Image missing" .