TY - JOUR AU - Rauber Du Bois, André AU - Ribeiro, Rodrigo AU - Amaro, Maycon PY - 2020/06/18 Y2 - 2024/03/28 TI - A Mechanized Proof of a Textbook Type Unification Algorithm JF - Revista de Informática Teórica e Aplicada JA - RITA VL - 27 IS - 3 SE - Regular Papers DO - 10.22456/2175-2745.100968 UR - https://seer.ufrgs.br/index.php/rita/article/view/Vol27_nr3_13 SP - 13-24 AB - <div class="page" title="Page 1"><div class="section"><div class="layoutArea"><div class="column"><div class="page" title="Page 1"><div class="section"><div class="layoutArea"><div class="column"><p><span>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 a formalization in Coq of a type unification algorithm that follows classic algorithms presented in programming language textbooks. We also report on the use of such formalization to build a correct type inference algorithm for the simply typed </span><span>λ</span><span>-calculus.</span></p></div></div></div></div></div></div></div></div> ER -