S. van Bakel and M. Dezani-Ciancaglini
Characterizing strong normalization for
explicit substitutions
In LATIN'02, volume 2286 of LNCS, pages 356-370
Springer-Verlag, 2002
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 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.
[ bib |
.pdf ]
Back
This file has been generated by
bibtex2html 1.43