Advisor: Yannick Forster
Subtyping and universal quantification are two orthogonal features often desired in a type system, and ubiquitous among programming languages. The combination of both these features gives rise to bounded quantification which restricts type abstraction so that only subtypes of a given bound can be used to instantiate. As System F formalizes universal quantification, the type system formalizing bounded quantification is called System F<:. Pierce [1] shows that bounded quantification makes subtyping and type checking undecidable in System F<:. The proof consists of a series of refinements to System F<: without arrow types, as they are not necessary to show undecidability. The subtyping relation on the refined system is shown to coincide with the full system while being able to encode the transition function of an intermediate machine model; the rowing machines. Finally the halting problem of rowing machines is shown to be many-one reducible from the halting problem of two-counter machines, which is a well-known undecidable problem. In this work we give a machine-checked presentation of Pierce’s proof using the synthetic approach of the Coq Library of Undecidability Proofs. The mechanization is built around syntax produced by Autosubst 2 as the tool provides several useful variants of syntax that significantly simplify the proof. In particular we use unscoped and well-scoped syntax, alongside with polyadic binders, and show how to encode them appropriately using bounded extensionality. We formalize Pierce’s proof showing explicitly the necessary inductive arguments in each step, for example complete induction on the height of derivations, the details of which are glossed over in the textbook presentation. Finally, we describe several mechanization artifacts that are unrelated to the mathematical argument but are nevertheless interesting as they simplify the machine-checked proof.