Paper Info
Title
A Mechanized Textbook Proof of a Type Unification Algorithm.
Abstract
Unification is the core of type inference algorithms for modern functional programming languages, like Haskell. 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.
Year
Venue
Field
2015
SBMF
Domain-specific language,Programming language,Functional programming,Computer science,Unification,Type inference,Theoretical computer science,Haskell,Proof obligation,Proof assistant
DocType
Citations 
PageRank 
Conference
0
0.34
References 
Authors
10
2
Name
Order
Citations
PageRank
Rodrigo Ribeiro100.68
Carlos Camarão2175.74