A mechanized proof of a textbook type unification algorithm.
Nenhuma Miniatura disponível
Data
2020
Título da Revista
ISSN da Revista
Título de Volume
Editor
Resumo
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 λ-calculus.
Descrição
Palavras-chave
Coq proof assistant, Assistente de provas Coq
Citação
AMARO, 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.