A mechanized proof of a textbook type unification algorithm.
dc.contributor.author | Amaro, Maycon José Jorge | |
dc.contributor.author | Ribeiro, Rodrigo Geraldo | |
dc.contributor.author | Bois, André Rauber Du | |
dc.date.accessioned | 2022-02-15T16:07:24Z | |
dc.date.available | 2022-02-15T16:07:24Z | |
dc.date.issued | 2020 | pt_BR |
dc.description.abstract | 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. | pt_BR |
dc.description.abstracten | A unificação é um componente central de algoritmos de inferência de tipos presentes em linguagens funcionais modernas, como Haskell e SML. Esse trabalho relata os primeiros passos em direção a formalização, usando o assistente de provas Coq, de um algoritmo de inferência de tipos conforme este é apresentado em livros texto da área de linguagens de programação. A partir do algoritmo formalizado, descrevemos uma implementação de um algoritmo de inferência de tipos para o λ-cálculo simplesmente tipado. | pt_BR |
dc.identifier.citation | 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. | pt_BR |
dc.identifier.doi | https://doi.org/10.22456/2175-2745.100968 | pt_BR |
dc.identifier.uri | http://www.repositorio.ufop.br/jspui/handle/123456789/14494 | |
dc.language.iso | en_US | pt_BR |
dc.rights | aberto | pt_BR |
dc.rights.license | This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License. Fonte: o PDF do artigo. | pt_BR |
dc.subject | Coq proof assistant | pt_BR |
dc.subject | Assistente de provas Coq | pt_BR |
dc.title | A mechanized proof of a textbook type unification algorithm. | pt_BR |
dc.title.alternative | Uma prova de correção formalmente verificada de um algoritmo de unificação de tipos. | pt_BR |
dc.type | Artigo publicado em periodico | pt_BR |
Arquivos
Pacote Original
1 - 1 de 1
Nenhuma Miniatura disponível
- Nome:
- ARTIGO_MechanizedProofTextbook.pdf
- Tamanho:
- 228.3 KB
- Formato:
- Adobe Portable Document Format
- Descrição:
Licença do Pacote
1 - 1 de 1
Nenhuma Miniatura disponível
- Nome:
- license.txt
- Tamanho:
- 1.71 KB
- Formato:
- Item-specific license agreed upon to submission
- Descrição: