Bounded quantification is undecidable
typed \(\lambda\)-calculus with subtyping and bounded second-order polymorphism
reduction from the halting problem for two-counter Turing machines
scientific article; zbMATH DE number 591677