Termination of System F-bounded: A Complete Proof

Abstract

System F-bounded is a second-order typed λ-calculus with subtyping which has been defined to carry out foundational studies about the type systems of object-oriented languages. The almost recursive nature of the essential feature of this system makes one wonder whether it retains the strong normalization property, with respect to first- and second-order βη reduction of system F≤. We prove that this is the case. The proof is carried out to the last detail to allow the reader to be convinced of its correctness. © 1997 Academic Press.