Cut-Elimination in the Strict Intersection Type Assignment System is Strongly Normalizing
van Bakel, Steffen
Notre Dame J. Formal Logic, Tome 45 (2004) no. 1, p. 35-63 / Harvested from Project Euclid
Text on Project Euclid
PDF
Alt PDF
This paper defines reduction on derivations (cut-elimination) in the Strict Intersection Type Assignment System of an earlier paper and shows a strong normalization result for this reduction. Using this result, new proofs are given for the approximation theorem and the characterization of normalizability of terms using intersection types.
Publié le : 2004-01-14
Classification:  intersection types,  lambda calculus,  termination,  cut-elimination,  03B15,  03F05,  68Q55 
@article{1094155278,
     author = {van Bakel, Steffen},
     title = {Cut-Elimination in the Strict Intersection Type Assignment System is Strongly Normalizing},
     journal = {Notre Dame J. Formal Logic},
     volume = {45},
     number = {1},
     year = {2004},
     pages = { 35-63},
     language = {en},
     url = {http://dml.mathdoc.fr/item/1094155278}
}

van Bakel, Steffen. Cut-Elimination in the Strict Intersection Type Assignment System is Strongly Normalizing. Notre Dame J. Formal Logic, Tome 45 (2004) no. 1, pp.  35-63. http://gdmltest.u-ga.fr/item/1094155278/