Paper: Typability and type checking in the second-order λ-calculus are equivalent and undecidable (at LICS 1994)
Authors: J. B. WellsAbstract
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 = {J. B. Wells}, title = {Typability and type checking in the second-order λ-calculus are equivalent and undecidable }, booktitle = {Proceedings of the Ninth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1994}, year = 1994, editor = {Samson Abramsky}, month = {July}, pages = {176--185}, location = {Paris, France}, publisher = {IEEE Computer Society Press} }