Reference. Typability and type checking in the second-order λ-calculus are equivalent and undecidable [wells-1994-typability]

1994 · J. B. Wells · 10.1109/lics.1994.316068 
@inproceedings{wells-1994-typability,
	author = {Wells, J.B.},
	title = {Typability and type checking in the second-order $\lambda$-calculus are equivalent and undecidable},
	booktitle = {Proceedings Ninth Annual IEEE Symposium on Logic in Computer Science},
	year = {1994},
	pages = {176--185},
	publisher = {IEEE Comput. Soc. Press},
	address = {Paris, France},
	doi = {10.1109/lics.1994.316068},
	url = {https://doi.org/10.1109/lics.1994.316068}
}