TERMINATION OF SYSTEM F-BOUNDED - A COMPLETE PROOF

System F-bounded is a second-order typed lambda-calculus with subtypin g which has been defined to carry out foundational studies about the t ype systems of object-oriented languages. The almost recursive nature of the essential feature of this system makes one wonder whether it re tains the strong normalization property, with respect to first- and se cond-order beta eta reduction of system F-less than or equal to. We pr ove that this is the case. The proof is carried out to the last detail to allow the reader to be convinced of its correctness. (C) 1997 Acad emic Press.