A Mechanized Textbook Proof of a Type Unification Algorithm

Unification is the core of type inference algorithms for modern functional programming languages, like Haskell. As a first step towards a formalization of a type inference algorithm for such programming languages, we present a formalization in Coq of a type unification algorithm that follows classic algorithms presented in programming language textbooks.