A Coq Formalization of Boolean Unification

We report on a verified implementation of two (well-known) algorithms for unification modulo the theory of Boolean rings: Löwenheim’s method and the method of Successive Variable Elimination. The implementations and proofs of correctness were done in the Coq proof assistant; we view this contribution as an early step in a larger project of developing a suite of verified implementations of equational unification algorithms.