WPI - Computer Science Department, Yichi Xu " A Coq Formalization of Unification Modulo Exclusive-Or"
Department(s):
Computer ScienceYichi 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.