J. B. Wells
Typability and Type-Checking in the Second-Order λ-Calculus are Equivalent and Undecidable
LICS, 1994.
@inproceedings{LICS-1994-Wells, author = "J. B. Wells", booktitle = "{Proceedings of the Ninth Annual Symposium on Logic in Computer Science}", doi = "10.1109/LICS.1994.316068", isbn = "0-8186-6310-3", pages = "176--185", publisher = "{IEEE Computer Society}", title = "{Typability and Type-Checking in the Second-Order λ-Calculus are Equivalent and Undecidable}", year = 1994, }