Amaro, Maycon José JorgeRibeiro, Rodrigo GeraldoBois, André Rauber Du2022-02-152022-02-152020AMARO, M. J. J.; RIBEIRO, R. G.; BOIS, A. R. D. A mechanized proof of a textbook type unification algorithm. Revista de Informática Teórica e Aplicada, v. 27, n. 3, p. 13-24, 2020. Disponível em: <https://seer.ufrgs.br/rita/article/view/Vol27_nr3_13>. Acesso em: 25 ago. 2021.http://www.repositorio.ufop.br/jspui/handle/123456789/14494Unification 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 λ-calculus.en-USabertoCoq proof assistantAssistente de provas CoqArtigo publicado em periodicoThis work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License. Fonte: o PDF do artigo.https://doi.org/10.22456/2175-2745.100968