Advisor: Yannick Forster
Supervisor: Gert Smolka
In this thesis we formally verify the undecidability of higher-order unification in the proof assistant Coq. Higher-order unification procedures underlie many modern day proof assistants including Coq. Higher-order unification is the process of finding an instantiation of the free variables in two typed terms such that after substitution the resulting terms are convertible.
While it is well-known that unification of first-order terms is decidable, for terms of higher order the problem has been shown to be undecidable. In 1973 Gerard Huet proved that third-order unification is undecidable with a reduction from the Post correspondence problem. Warren D. Goldfarb improved on this result in 1981 by proving that even unification in second-order languages is undecidable. The proof is obtained by a reduction from Hilbert's tenth problem.
In this work we formalise both reductions in Coq. We simplify Huet's proof by reducing from the modified Post correspondence problem and give an intuitive explanation of Goldfarb's construction. Furthermore, we show that the undecidability of second and third-order unification is sufficient to conclude the undecidability of higher-order unification in general and how Huet's result can be obtained as a corollary of Goldfarb's result.