1. REPOSITORIO INSTITUCIONAL DA UFOP
  2. ICEB - Instituto de Ciências Exatas e Biológicas
  3. DECOM - Departamento de Computação
  4. DECOM - Artigos publicados em periódicos
Use este identificador para citar ou linkar para este item: http://www.repositorio.ufop.br/jspui/handle/123456789/14494
Registro completo de metadados
Campo Dublin CoreValorIdioma
dc.contributor.authorAmaro, Maycon José Jorge-
dc.contributor.authorRibeiro, Rodrigo Geraldo-
dc.contributor.authorBois, André Rauber Du-
dc.date.accessioned2022-02-15T16:07:24Z-
dc.date.available2022-02-15T16:07:24Z-
dc.date.issued2020pt_BR
dc.identifier.citationAMARO, 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.urihttp://www.repositorio.ufop.br/jspui/handle/123456789/14494-
dc.description.abstractUnification 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.language.isoen_USpt_BR
dc.rightsabertopt_BR
dc.subjectCoq proof assistantpt_BR
dc.subjectAssistente de provas Coqpt_BR
dc.titleA mechanized proof of a textbook type unification algorithm.pt_BR
dc.title.alternativeUma prova de correção formalmente verificada de um algoritmo de unificação de tipos.pt_BR
dc.typeArtigo publicado em periodicopt_BR
dc.rights.licenseThis work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License. Fonte: o PDF do artigo.pt_BR
dc.description.abstractenA 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.doihttps://doi.org/10.22456/2175-2745.100968pt_BR
Aparece nas coleções:DECOM - Artigos publicados em periódicos

Arquivos associados a este item:
Arquivo Descrição TamanhoFormato 
ARTIGO_MechanizedProofTextbook.pdf228,3 kBAdobe PDFVisualizar/Abrir
Mostrar registro simples do item Visualizar estatísticas


Os itens no repositório estão protegidos por copyright, com todos os direitos reservados, salvo quando é indicado o contrário.