André Rauber Du Bois

A Mechanized Proof of a Textbook Type Unification Algorithm

2020 · Revista de Informática Teórica e Aplicada

Unification is the core of type inference algorithms for modern functional programming languages, like Haskell and SML. As a first step towards a formalization of a type inference algorithm for such programming languages, we present …