Termination of SystemF-bounded: A Complete Proof

SystemF-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 systemF ⩽. 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.

Authors

• Giorgio Ghelli

Keywords

No keywords are indexed for this paper.