| for Explicit Substitutions Abstract (2008) | |||||||||||||||
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. | |||||||||||||||
Details der Publikation | |||||||||||||||
| |||||||||||||||