Characterising strong normalisation for explicit substitutions

Abstract

We characterise the strongly normalising terms of a composition-free calculus of explicit substitutions (with or without garbage collection) by means of an intersection type assignment system. The main novelty is a 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.