Thomas Neele: Operations on Fixpoint Equation Systems, a formalisation in Coq.


Event Details


Fixpoint equation systems over arbitrary complete lattices generalise several established formalisms such as parity games and parameterised Boolean equation systems. We identify a number of elementary operations, such as swapping equations and substituting variables by their definitions and prove their correctness. All proofs are formalised in Coq. In this talk, I will go into the history of this work, introduce fixpoint equation systems, show how these can be formalised in Coq, demo a couple of Coq proofs, and highlight several Coq features.