Show simple item record

dc.contributor.authorKfoury, Assaf J.en_US
dc.contributor.authorPericas-Geertsen, Santiago M.en_US
dc.date.accessioned2011-10-20T05:09:46Z
dc.date.available2011-10-20T05:09:46Z
dc.date.issued2000-03-06en_US
dc.identifier.citationKfoury, 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: http://hdl.handle.net/2144/1801]en_US
dc.identifier.urihttp://hdl.handle.net/2144/1801
dc.description.abstractWe 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.sponsorshipNational Science Foundation (CCR-9417382, EIA-9806745)en_US
dc.language.isoen_USen_US
dc.publisherBoston University Computer Science Departmenten_US
dc.relation.ispartofseriesBUCS Technical Reports;BUCS-TR-2000-007en_US
dc.subjectType systemsen_US
dc.subjectType inferenceen_US
dc.subjectLambda calculusen_US
dc.subjectUnificationen_US
dc.subjectSoftware specificationen_US
dc.titleType Inference For Recursive Definitionsen_US
dc.typeTechnical Reporten_US


Files in this item

This item appears in the following Collection(s)

Show simple item record