Decidability and Confluence of βη top≤ Reduction in F≤

AbstractWe contribute to the syntactic study of F≤, a variant of second-order λ-calculus F which appears as a paradigmatic kernel language for polymorphism and subtyping. The type system of F≤ has a maximum type Top and bounded quantification. We endow this language with the β-rules (for terms and types), to which we add η-rules (for terms and types) and a rule which equates all terms of type Top. These rules are suggested by the axiomatization of cartesian closed categories. We exhibit a weakly normalizing and confluent reduction system for this theory βη top≤, and show that it is decidable. It is also confluent, but decidability does not follow from confluence, since reduction is not effective. Our proofs rely on the confluence and decidability of a corresponding system on F1 (the extension of F with a terminal type)