Factoring Derivation Spaces via Intersection Types (Extended Version)

Pablo Barenbaum, Gonzalo Ciruelos

In typical non-idempotent intersection type systems, proof normalization is not confluent. In this paper we introduce a confluent non-idempotent intersection type system for the la…