DECOM - Artigos publicados em periódicos
URI Permanente para esta coleção
Navegar
Navegando DECOM - Artigos publicados em periódicos por Autor "Amaro, Maycon José Jorge"
Agora exibindo 1 - 2 de 2
Resultados por página
Opções de Ordenação
Item A mechanized proof of a textbook type unification algorithm.(2020) Amaro, Maycon José Jorge; Ribeiro, Rodrigo Geraldo; Bois, André Rauber DuUnification 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.Item The design of a verified derivative-based parsing tool for regular expressions.(2021) Cardoso, Elton Máximo; Amaro, Maycon José Jorge; Feitosa, Samuel da Silva; Reis, Leonardo Vieira dos Santos; Bois, André Rauber Du; Ribeiro, Rodrigo GeraldoWe describe the formalization of Brzozowski and Antimirov derivative based algorithms for regular expression parsing, in the dependently typed language Agda. The formalization produces a proof that either an input string matches a given regular expression or that no matching exists. A tool for regular expression based search in the style of the well known GNU grep has been developed with the certified algorithms. Practical experiments conducted with this tool are reported.