Higher-order subtyping and its decidability

We define the typed lambda calculus F ω ∧ (F-omega-meet), a natural generalization of Girard's system F ω (F-omega) with intersection types and bounded polymorphism. A novel aspect of our presentation is the use of term rewriting techniques to present intersection types, which clearly splits the computational semantics (reduction rules) from the syntax (inference rules) of the system. We establish properties such as Church-Rosser for the reduction relation on types and terms, and strong normalization for the reduction on types. We prove that types are preserved by computation (subject reduction), and that the system satisfies the minimal types property. We define algorithms for type checking and subtype checking. The development culminates with the proof of decidability of typing in F ω ∧, containing the first proof of decidability of subtyping of a higher-order lambda calculus with subtyping.

Authors

• Adriana Compagnoni

Keywords

• Higher-order lambda calculus
• Higher-order subtyping
• Intersection types
• Bounded polymorphism
• Decidability