# Factoring Derivation Spaces via Intersection Types (Extended Version)

## TL;DR

This paper introduces a confluent non-idempotent intersection type system for lambda-calculus that enables unique factorization of derivation spaces into garbage-free and garbage parts, improving understanding of resource usage.

## Contribution

It presents a novel confluent intersection type system with proof term syntax, establishing a unique factorization of derivation spaces using a Grothendieck construction.

## Key findings

- The system enjoys subject reduction and strong normalization.
- Derivation spaces can be uniquely factorized into garbage-free and garbage parts.
- A correspondence with lambda-calculus via simulation theorems is established.

## Abstract

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 lambda-calculus. Typing derivations are presented using proof term syntax. The system enjoys good properties: subject reduction, strong normalization, and a very regular theory of residuals. A correspondence with the lambda-calculus is established by simulation theorems. The machinery of non-idempotent intersection types allows us to track the usage of resources required to obtain an answer. In particular, it induces a notion of garbage: a computation is garbage if it does not contribute to obtaining an answer. Using these notions, we show that the derivation space of a lambda-term may be factorized using a variant of the Grothendieck construction for semilattices. This means, in particular, that any derivation in the lambda-calculus can be uniquely written as a garbage-free prefix followed by garbage.