Stéphane Lengrand, Pierre Lescanne, Daniel J. Dougherty,
Mariangiola Dezani-Ciancaglini, and Steffen van Bakel
Intersection types for explicit
substitutions
Inform. & Comput., 189(1):17-42, 2004
We present a new system of intersection types for a
composition-free calculus of explicit substitutions
with a rule for garbage collection, and show that it
characterizes those terms which are strongly
normalizing. This system extends previous work on
the natural generalization of the classical
intersection types system, which characterized head
normalization and weak normalization, but was not
complete for strong normalization. An important role
is played by the notion of available variable
in a term, which is a generalization of the
classical notion of free variable.
[ bib |
.pdf ]
Back
This file has been generated by
bibtex2html 1.43