Abstract

We characterise the strongly normalising terms of a composition-free calculus of explicit substititions (with or without garbage collection) by means of an intersection type assignment system. The main novelty is a new cut-rule which allows to forget the context of the minor premise when the context of the main premise does not have an assumption for the cut variable.

Appeared as:

@Inproceedings {Bakel-Dezani-LATIN'02,

Author = "S. van Bakel, M. Dezani-Ciacaglini.",
Title = "{C}haracterising {S}trong {N}ormalisation for {E}xplicit {S}ubstitutions",
Booktitle = "Proceedings of Latin American Theoretical Informatics (LATIN'02)",
Series = "Lecture Notes in Computer Science",
Publisher = "Springer-Verlag",
Volume = "2286",
Pages = "356-370",
Year = "2002"
}