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.