Speaker: Jaco van de Pol (FM, TU/e and CWI)
Title: Fixpoint Equation Systems

Abstract:
  Both Boolean Equation Systems (BES) and Parameterized Boolean
Equation Systems (PBES) are instances of Fixpoint Equation Systems
(FES) over arbitrary complete lattices. We show how a number of
basic theorems can be proven for FES, generalizing some results
from the literature on BES and PBES. These results include the
basic ingredients from Gauss elimination. We claim that the theory
and proofs are smoother at the FES level than at PBES level. FESs
can be easily formalized in higher-order logic. With relatively
little effort we could verify all our proofs in the interactive
theorem prover PVS.