Syntactic Metatheory of Higher-Order Subtyping

10 years 3 months ago
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.
Andreas Abel, Dulma Rodriguez
Added 19 Oct 2010
Updated 19 Oct 2010
Type Conference
Year 2008
Where CSL
Authors Andreas Abel, Dulma Rodriguez
Comments (0)