Type Inference For Recursive Definitions


Show simple item record Kfoury, Assaf J. en_US Pericas-Geertsen, Santiago M. en_US 2011-10-20T05:09:46Z 2011-10-20T05:09:46Z 2000-03-06 en_US
dc.identifier.citation Kfoury, Assaf; Pericas-Geertsen, Santiago M.. "Type Inference For Recursive Definitions", Technical Report BUCS-2000-007, Computer Science Department, Boston University, March 6, 2000. [Available from:] en_US
dc.description.abstract We consider type systems that combine universal types, recursive types, and object types. We study type inference in these systems under a rank restriction, following Leivant's notion of rank. To motivate our work, we present several examples showing how our systems can be used to type programs encountered in practice. We show that type inference in the rank-k system is decidable for k ≤ 2 and undecidable for k ≥ 3. (Similar results based on different techniques are known to hold for System F, without recursive types and object types.) Our undecidability result is obtained by a reduction from a particular adaptation (which we call "regular") of the semi-unification problem and whose undecidability is, interestingly, obtained by methods totally different from those used in the case of standard (or finite) semi-unification. en_US
dc.description.sponsorship National Science Foundation (CCR-9417382, EIA-9806745) en_US
dc.language.iso en_US en_US
dc.publisher Boston University Computer Science Department en_US
dc.relation.ispartofseries BUCS Technical Reports;BUCS-TR-2000-007 en_US
dc.subject Type systems en_US
dc.subject Type inference en_US
dc.subject Lambda calculus en_US
dc.subject Unification en_US
dc.subject Software specification en_US
dc.title Type Inference For Recursive Definitions 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


Deposit Materials