**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.

**Gérard P. Huet.***The undecidability of unification in third order logic.*Information and control, 22(3):257-267, 1973.**Warren D. Goldfarb.**The undecidability of the second-order unification problem. Theoretical Computer Science, 13:225-230, 1981.**Gilles Dowek.**Higher-order unification and matching. Handbook of automated reasoning, 2:1009-1062, 2001.**Wayne Snyder and Jean H Gallier.**Higher order unification revisited: Complete sets of transformations. Technical Reports (CIS), page 778, 1989.**Yannick Forster, Dominik Kirst, and Gert Smolka.**On synthetic undecidability in Coq, with an application to the Entscheidungsproblem. In Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 38-51. ACM, 2019.

**Initial Talk:**Slides (2nd October 2018)**Second Talk:**Slides (14th December 2018)**Final Talk:**Slides, Handout (14th December 2018)**Source Code:**CoqDoc, Source Code (GitHub)**Thesis:**Thesis (29th March 2019)