A Mechanized textbook proof of a type unification algorithm

Published in Formal Methods: Foundations and Applications - 18th Brazilian Symposium on Formal Methods., 2016

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.

Download paper here