OpenBU

A Direct Algorithm for the Type Interference in the Rank 2 Fragment of the Second--Order λ-Calculus

OpenBU

Show simple item record

dc.contributor.author Kfoury, A. J.
dc.contributor.author Wells, J. B.
dc.date.accessioned 2011-09-12T15:28:39Z
dc.date.available 2011-09-12T15:28:39Z
dc.date.issued 1993-12-01
dc.identifier.uri http://hdl.handle.net/2144/1475
dc.description.abstract We study the problem of type inference for a family of polymorphic type disciplines containing the power of Core-ML. This family comprises all levels of the stratification of the second-order lambda-calculus by "rank" of types. We show that typability is an undecidable problem at every rank k ≥ 3 of this stratification. While it was already known that typability is decidable at rank ≤ 2, no direct and easy-to-implement algorithm was available. To design such an algorithm, we develop a new notion of reduction and show how to use it to reduce the problem of typability at rank 2 to the problem of acyclic semi-unification. A by-product of our analysis is the publication of a simple solution procedure for acyclic semi-unification. en_US
dc.language.iso en_US en_US
dc.publisher Boston University Department of Computer Science en_US
dc.relation.ispartofseries BUCS;BUCS-TR-1993-017
dc.subject Technical Report, Computer Science en_US
dc.title A Direct Algorithm for the Type Interference in the Rank 2 Fragment of the Second--Order λ-Calculus en_US
dc.type Technical Report en_US


Files in this item

This item appears in the following Collection(s)

Show simple item record

Search OpenBU


Browse

Deposit Materials

Statistics