System Fi A Higher-Order Polymorphic λ-Calculus with Erasable Term-Indices

We introduce a foundational lambda calculus, System F-i, for studying programming languages with term-indexed datatypes - higher-kinded datatypes whose indices range over data such as natural numbers or lists. System F-i is an extension of System F-i that introduces the minimal features needed to support term-indexing. We show that System F-i provides a theory for analysing programs with term-indexed types and also argue that it constitutes a basis for the design of logicallysound light-weight dependent programming languages. We establish erasure properties of F-i-types that capture the idea that term-indices are discardable in that they are irrelevant for computation. Index erasure projects typing in System F-i to typing in System F-i. So, System F-i inherits strong normalization and logical consistency from System F-i.