A mechanized proof of a textbook type unification algorithm.

Registro completo de metadados
MetadadosDescriçãoIdioma
Autor(es): dc.creatorAmaro, Maycon José Jorge-
Autor(es): dc.creatorRibeiro, Rodrigo Geraldo-
Autor(es): dc.creatorBois, André Rauber Du-
Data de aceite: dc.date.accessioned2025-08-21T15:05:57Z-
Data de disponibilização: dc.date.available2025-08-21T15:05:57Z-
Data de envio: dc.date.issued2022-02-14-
Data de envio: dc.date.issued2022-02-14-
Data de envio: dc.date.issued2019-
Fonte completa do material: dc.identifierhttp://www.repositorio.ufop.br/jspui/handle/123456789/14494-
Fonte completa do material: dc.identifierhttps://doi.org/10.22456/2175-2745.100968-
Fonte: dc.identifier.urihttp://educapes.capes.gov.br/handle/capes/1002385-
Descrição: dc.descriptionUnification 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: dc.descriptionA 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.-
Formato: dc.formatapplication/pdf-
Idioma: dc.languageen-
Direitos: dc.rightsaberto-
Direitos: dc.rightsThis work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License. Fonte: o PDF do artigo.-
Palavras-chave: dc.subjectCoq proof assistant-
Palavras-chave: dc.subjectAssistente de provas Coq-
Título: dc.titleA mechanized proof of a textbook type unification algorithm.-
Título: dc.titleUma prova de correção formalmente verificada de um algoritmo de unificação de tipos.-
Aparece nas coleções:Repositório Institucional - UFOP

Não existem arquivos associados a este item.