Order-Sorted Inductive Types

SystemF ω ⩽is an extension of systemF ω with subtyping and bounded quantification. Order-sorted algebra is an extension of many-sorted algebra with overloading and subtyping. We combine both formalisms to obtainIF ω ⩽, a higher-order typedλ-calculus with subtyping, bounded quantification, and order-sorted inductive types, i. e. , data types with built-in subtyping and overloading. Moreover we show thatIF ω ⩽enjoys important meta-theoretic properties, including confluence, strong normalization, subject reduction, and decidability of type checking.

Authors

• Gilles Barthe

Keywords

No keywords are indexed for this paper.