Intersection type systems and explicit substitutions calculi

Abstract

The λ-calculus with de Bruijn indices, called λdB , assembles each α-class of λ-terms into a unique term, using indices instead of variable names. Intersection types provide finitary type polymorphism satisfying important properties like principal typing, which allows the type system to include features such as data abstraction (modularity) and separate compilation. To be closer to computation and to simplify the formalisation of the atomic operations involved in β-contractions, several explicit substitution calculi were developed most of which are written with de Bruijn indices. Although untyped and simply types versions of explicit substitution calculi are well investigated, versions with more elaborate type systems (e.g., with intersection types) are not. In previous work, we presented a version for λdB of an intersection type system originally introduced to characterise principal typings for β-normal forms and provided the characterisation for this version. In this work we introduce intersection type systems for two explicit substitution calculi: the λσ and the λse . These type system are based on a type system for λdB and satisfy the basic property of subject reduction, which guarantees the preservation of types during computations. © 2010 Springer-Verlag.