Typability and type checking in System F are equivalent and undecidable
second-order polymorphically typed lambda calculus
scientific article; zbMATH DE number 1340811
scientific article