Bounded quantification is undecidable

Abstract: "F[less than or equal to] is a typed [lambda]-calculus with subtyping and bounded second-order polymorphism. First introduced by Cardelli and Wegner, it has been widely studied as a core calculus for type systems with subtyping. Curien and Ghelli proved the partial correctness of a recursive procedure for computing minimal types of F[less than or equal to] terms and showed that the termination of this procedure is equivalent to the termination of its major component, a procedure for checking the subtype relation between F[less than or equal to] types.Ghelli later claimed that this procedure is also guaranteed to terminate, but the discovery of a subtle bug in his proof led him recently to observe that, in fact, there are inputs on which the subtyping procedure diverges. This reopens the question of the decidability of subtyping and hence of typechecking. This question is settled here in the negative, using a reduction from the halting problem for two-counter Turing machines to show that the subtype relation of F[less than or equal to] is undecidable."