Advisors: Gert Smolka, Yannick Forster
The problem of unifying terms naturally arises when working in type theory
like in the proof assistant Coq. Two terms are said to be unifiable if there is a
substitution such that these terms have the same normal form under the
substitution. For first-order terms it is well known that this problem is
decidable. For higher-order terms it has been shown that unification is
In 1973 Gerard Huet proved that 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 second-order unification is undecidable. The proof is obtained by a reduction from Hilbert's 10th problem – Diophantine Equations – to second-order unification.
In my Bachelor's thesis I want to formalise both reductions in Coq. In this talk I will give some insight into the essence of the Huet reduction. Additionally I will shortly explain the main idea of the Goldfarb reduction.