Intersection Type Systems and Explicit Substitutions Calculi

摘要

The A-calculus with de Bruijn indices, called λ_dB, assembles each a-class of A-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 Ads 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 Act and the λs_e. These type system are based on a type system for λd_B and satisfy the basic property of subject reduction, which guarantees the preservation of types during computations.