publication . Article . 2020

A Mechanized Proof of a Textbook Type Unification Algorithm

André Rauber Du Bois; Rodrigo Ribeiro; Maycon Amaro;
Open Access
  • Published: 18 Jun 2020 Journal: Revista de Informática Teórica e Aplicada, volume 27, pages 13-24 (issn: 0103-4308, eissn: 2175-2745, Copyright policy)
  • Publisher: Universidade Federal do Rio Grande do Sul
Abstract
<jats:p>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.</jats:p>
Subjects
ACM Computing Classification System: TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMSTheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES
free text keywords: Computer Science; formal verification ; compilers, Type inference; unification; Coq proof assistant
Powered by OpenAIRE Research Graph
Any information missing or wrong?Report an Issue