Syntactic Metatheory of Higher-Order Subtyping

Abstract. We present a new proof of decidability of higher-order subtyping in the presence of bounded quantification. The algorithm is formulated as a judgement which operates on beta-eta-normal forms. Transitivity and closure under application are proven directly and syntactically, without the need for a model construction or reasoning on longest beta-reduction sequences. The main technical tool is hereditary substitution, i.e., substitution of one normal form into another, resolving all freshly generated redexes on the fly. Hereditary substitutions are used to keep types in normal-form during execution of the subtyping algorithm. Termination of hereditary substitutions can be proven in an elementary way, by a lexicographic induction on the kind of the substituted variable and the size of the expression substituted into--this is what enables a purely syntactic metatheory.

• Type: Conference
• Year: 2008
• Where: CSL
• Authors: Andreas Abel, Dulma Rodriguez
• Keywords: Automated Reasoning, CSL 2008, Hereditary Substitutions, Longest Beta-reduction Sequences, Main Technical Tool