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.
Termination of system F-bounded: a complete proof
GHELLI, GIORGIO
1997-01-01
Abstract
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.File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
