• DocumentCode
    2720675
  • Title

    The subtyping problem for second-order types is undecidable

  • Author

    Tiuryn, Jerzy ; Urzyczyn, Pawel

  • Author_Institution
    Inst. of Inf., Warsaw Univ., Poland
  • fYear
    1996
  • fDate
    27-30 Jul 1996
  • Firstpage
    74
  • Lastpage
    85
  • Abstract
    We prove that the subtyping problem induced by Mitchell´s containment relation (1988) for second-order polymorphic types is undecidable. It follows that type-checking is undecidable for the polymorphic lambda-calculus extended by an appropriate subsumption rule
  • Keywords
    decidability; lambda calculus; programming theory; type theory; containment relation; polymorphic lambda-calculus; second-order polymorphic types; second-order types; subsumption rule; subtyping problem; type-checking; Iron; Terminology;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Logic in Computer Science, 1996. LICS '96. Proceedings., Eleventh Annual IEEE Symposium on
  • Conference_Location
    New Brunswick, NJ
  • ISSN
    1043-6871
  • Print_ISBN
    0-8186-7463-6
  • Type

    conf

  • DOI
    10.1109/LICS.1996.561306
  • Filename
    561306
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=2720675