Bounding normalization time through intersection types
Erika De Benedetti, Benedetti Simona, Ronchi Della Rocca · 2013
Intersection types were originally introduced as idempotent, i.e., modulo the equivalence σ ∧σ = σ. In fact, they have been used essentially for semantic purposes, for building filter models for λ-calculus, where the interpretation of types as properties of terms induces naturally the idempotence property. Recently it has been observed that, when dropping idempotency, intersection types can be used for rea-