Thumbnail
Access Restriction
Subscribed

Author Pottier, François ♦ Gauthier, Nadji
Source ACM Digital Library
Content type Text
Publisher Association for Computing Machinery (ACM)
File Format PDF
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Computer programming, programs & data
Subject Keyword Unification ♦ Recursive types ♦ Equality ♦ Polymorphism
Abstract We study a type system equipped with universal types and equire-cursive types, which we refer to as F͘. We show that type equality may be decided in time O(nlog n), an improvement over the previous known bound of $O(n^{2}$ ). In fact, we show that two more general problems, namely entailment of type equations and type unification, may be decided in time O(nlog n), a new result. To achieve this bound, we associate, with every F͘ type, a first-order canonical form, which may be computed in time O(nlogn). By exploiting this notion, we reduce all three problems to equality and unification of first-order recursive terms, for which efficient algorithms are known.
Description Affiliation: INRIA (Gauthier, Nadji; Pottier, François)
Age Range 18 to 22 years ♦ above 22 year
Educational Use Research
Education Level UG and PG
Learning Resource Type Article
Publisher Date 1983-05-01
Publisher Place New York
Journal ACM SIGPLAN Notices (SIGP)
Volume Number 39
Issue Number 9
Page Count 12
Starting Page 150
Ending Page 161


Open content in new tab

   Open content in new tab
Source: ACM Digital Library