Explicit substitution calculi with de Bruijn indices and intersection type systems

Explicit substitution calculi propose solutions to the main drawback of the λ-calculus: substitution defined as a metaoperation in the system. By making explicit the process of substitution, the theoretical system gets closer to an eventual implementation. Furthermore, for implementation purposes, many explicit substitution systems are written with de Bruijn indices. The λ-calculus with de Bruijn indices, called λdB, assembles each α-class of λ-terms in a unique term, which is more 'machine-friendly' than the classical version with variables. Intersection types (IT) provide finitary type polymorphism satisfying important properties like principal typing (PT), which allows the type system to include features such as data abstraction (modularity) and separate compilation. Although some explicit substitution calculi with simple type systems are well investigated, providing nice applications such as specialized implementations of higher order unification, more elaborated type systems such as IT have not been proposed/studied for these calculi. In an earlier work, we introduced IT systems for two explicit substitution calculi, λσ and λse, conjecturing them to satisfy the basic property of subject reduction (SR), which guarantees the preservation of types during computations. In this article, we take a deeper look at these systems, providing an insight into their development which helps us construct for the first time the proofs of SR omitted before. This new result also (i) enables us to prove another new result: SR for an IT system for λdB; and (ii) allows us to introduce for the first time an IT system for the λυ-calculus.