Typability and Type Checking in System F are Equivalent and Undecidable

J. B. Wells. Typability and Type Checking in System F are Equivalent and Undecidable. Annals of Pure and Applied Logic, 98(1-3):111-156, 1999.

Abstract

Abstract is missing.