WPI - Computer Science Department, Yichi Xu " A Coq Formalization of Unification Modulo Exclusive-Or"


Computer Science

Yichi Xu

MS Student

WPI – Computer Science


Thursday, April 20, 2023

Time: 11:00 a.m. 12:00 p.m.

Location: Fuller Labs 320

MS Thesis Advisor : Prof. Daniel Dougherty

Thesis Reader:   Prof. Rose Bohrer

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 a function with the   properties Associativity, Commutativity, Nilpotency, and the  presence of an identity.

 We   implement in Coq an algorithm inspired by Liu and  Lynch's inference rules, and prove it sound, complete, and terminating in Coq.   Using Coq's   code extraction capability one obtains an implementation in the programming language Ocaml.