Type Inference For Recursive Definitions


Show simple item record

dc.contributor.author Kfoury, Assaf J. en_US
dc.contributor.author Pericas-Geertsen, Santiago M. en_US
dc.date.accessioned 2011-10-20T05:09:46Z
dc.date.available 2011-10-20T05:09:46Z
dc.date.issued 2000-03-06 en_US
dc.identifier.uri http://hdl.handle.net/2144/1801
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

Advanced Search


Deposit Materials