System F-bounded is a second-order typed lambda-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 beta eta reduction of system F-less than or equal to. 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.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.