Strong Normalization through Intersection Types and Memory
Antonio Bucciarelli, Delia Kesner, Daniel Lima Ventura · Electronic Notes in Theoretical Computer Science · 2016
We characterize β -strongly normalizing λ -terms by means of a non-idempotent intersection type system. More precisely, we first define a memory calculus K together with a non-idempotent intersection type system K , and we show that a K-term t is typable in K if and only if t is K-strongly normalizing. We then show that β -strong normalization is equivalent to K-strong normalization. We conclude since λ -terms are strictly included in K-terms.