Non-idempotent types for classical calculi in natural deduction style

Delia Kesner, Pierre Vial

In the first part of this paper, we define two resource aware typing systems for the λμ-calculus based on non-idempotent intersection and union types. The non-idempotent approach p…