Subtyping + extensionality: Confluence of beta-eta top in Fsub, extended abstract

We contribute to the syntactic study of F less-than-or-equal-to, a variant of second order lambda-calculus F which appears as a paradigmatic kernel language for polymorphism and subtyping. The type system of F less-than-or-equal-to has a maximum type Top and bounded quantification. We endow this language with the familiar beta-rules (for terms and types), to which we add extensionality rules: the eta-rules (for terms and types), and a rule (top) which equates all terms of type Top. These rules are suggested by the axiomatization of cartesian closed categories. We show that this theory beta-eta-top less-than-or-equal-to is decidable, by exhibiting an effectively weakly normalizing and confluent rewriting system for it. Our proof of confluence relies on the confluence of a corresponding system on F1 (the extension of F with a terminal type), and follows a general pattern that we investigate for itself in a separate paper.