Intersection type systems and explicit substitutions calculi

Daniel Lima Ventura, Mauricio Ayala-Rincón, Fairouz Kamareddine

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Citation (Scopus)


The ?-calculus with de Bruijn indices, called ?dB , assembles each a-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 ?s 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.

Original languageEnglish
Title of host publicationLogic, Language, Information and Computation - 17th International Workshop, WoLLIC 2010, Proceedings
Number of pages15
Volume6188 LNAI
Publication statusPublished - 2010
Event17th International Workshop on Logic, Language, Information and Computation - Brasilia, Brazil
Duration: 6 Jul 20109 Jul 2010

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume6188 LNAI
ISSN (Print)0302-9743


Conference17th International Workshop on Logic, Language, Information and Computation
Abbreviated title WoLLIC 2010


Dive into the research topics of 'Intersection type systems and explicit substitutions calculi'. Together they form a unique fingerprint.

Cite this