Mechanized textbook proof of a type unification algorithm


Unification is the core of type inference algorithms for mod- ern 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.


Source code