A Coq Formalization of Unification Modulo Exclusive-Or

TL;DR

This paper presents a formalization and implementation of an XOR unification algorithm in Coq, proving its correctness and extracting executable code in OCaml for applications in automated reasoning and security analysis.

Contribution

It provides the first Coq formalization of XOR unification, including proofs of soundness, completeness, and termination, with an extracted OCaml implementation.

Findings

Algorithm is sound, complete, and terminating.

Successfully extracted OCaml code from Coq formalization.

Applicable to automated theorem proving and security protocols.

Abstract

Equational Unification is a critical problem in many areas such as automated theorem proving and security protocol analysis. In this paper, we focus on XOR-Unification, that is, unification modulo the theory of exclusive-or. This theory contains an operator with the properties Associativity, Commutativity, Nilpotency, and the presence of an identity. In the proof assistant Coq, we implement an algorithm that solves XOR unification problems, whose design was inspired by Liu and Lynch, and prove it sound, complete, and terminating. Using Coq's code extraction capability we obtain an implementation in the programming language OCaml.