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 tem 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...

• Type: Journal
• Year: 2010
• Where: WOLLIC
• Authors: Daniel Lima Ventura, Mauricio Ayala-Rincón, Fairouz Kamareddine
• Keywords: Artificial Intelligence, Explicit Substitution Calculi, Intersection Type, Type System, WOLLIC 2010