Paper: Typability and type checking in the second-order λ-calculus are equivalent and undecidable (at LICS 1994)

Authors: Joe B. Wells

Abstract

The problems of typability and type checking exist for the Girard/Reynolds second-order polymorphic typed λ-calculus (also known as “system F”) when it is considered in the “Curry style” (where types are derived for pure λ-terms). Until now the decidability of these problems for F itself has remained unknown. We first prove that type checking in F is undecidable by a reduction from semi-unification. We then prove typability in F is undecidable by a reduction from type checking. Since the reduction from typability to type checking in F is already known, the two problems in F are equivalent (reducible to each other). The results hold for both the usual λK-calculus and the more restrictive λI-calculus

BibTeX

  @InProceedings{Wells-Typabilityandtypech,
    author = 	 {Joe B. Wells},
    title = 	 {Typability and type checking in the second-order λ-calculus are equivalent and undecidable },
    booktitle =  {Proceedings of the Ninth Annual IEEE Symposium on Logic in Computer Science (LICS 1994)},
    year =	 {1994},
    month =	 {July}, 
    pages =      {176--185},
    location =   {Paris, France}, 
    publisher =	 {IEEE Computer Society Press}
  }