Computing Publications

Publications Home » Intersection types for explicit s...

Intersection types for explicit substitutions

Lengrand, Pierre Lescanne, Dan Dougherty, Dezani Dezani-Ciancaglini, Steffen van Bakel

Journal Article
Information and Computation
Volume 189
Issue 1
pp.17–42
2004
Elsevier
DOI 10.1016/j.ic.2003.09.004
Abstract

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.

PDF of full publication (218 kilobytes)
(need help viewing PDF files?)
BibTEX file for the publication
N.B.
Conditions for downloading publications from this site.
 

pubs.doc.ic.ac.uk: built & maintained by Ashok Argent-Katwala.