Show simple item record

dc.contributor.authorWells, J. B.en_US
dc.date.accessioned2011-10-20T04:32:21Z
dc.date.available2011-10-20T04:32:21Z
dc.date.issued1995-12-10
dc.identifier.citationWells, J.B.. "The Undecidability of Mitchell's Subtyping Relationship“, Technical Report BUCS-1995-019, Computer Science Department, Boston University, December 10, 1995. [Available from: http://hdl.handle.net/2144/1578]
dc.identifier.urihttps://hdl.handle.net/2144/1578
dc.description.abstractMitchell defined and axiomatized a subtyping relationship (also known as containment, coercibility, or subsumption) over the types of System F (with "→" and "∀"). This subtyping relationship is quite simple and does not involve bounded quantification. Tiuryn and Urzyczyn quite recently proved this subtyping relationship to be undecidable. This paper supplies a new undecidability proof for this subtyping relationship. First, a new syntax-directed axiomatization of the subtyping relationship is defined. Then, this axiomatization is used to prove a reduction from the undecidable problem of semi-unification to subtyping. The undecidability of subtyping implies the undecidability of type checking for System F extended with Mitchell's subtyping, also known as "F plus eta".en_US
dc.description.sponsorshipNational Science Foundation (CCR-9113196, CCR-9417382)en_US
dc.language.isoen_US
dc.publisherBoston University Computer Science Departmenten_US
dc.relation.ispartofseriesBUCS Technical Reports;BUCS-TR-1995-019
dc.titleThe undecidability of Mitchell's subtyping relationshipen_US
dc.typeTechnical Reporten_US


This item appears in the following Collection(s)

Show simple item record