Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
436345 | Theoretical Computer Science | 2008 | 13 Pages |
Abstract
This paper gives a new proof for the approximation theorem and the characterisation of normalisability using intersection types for a system with ‘w and a ≤-relation that is contra-variant over arrow types. The technique applied is to define reduction on derivations and to show a strong normalisation result for this reduction. From this result, the characterisation of strong normalisation and the approximation result will follow easily; the latter, in its turn, will lead to the characterisation of (head) normalisability.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics