A type-assignment of linear erasure and duplication

We introduce LEM, a type-assignment system for the linear λ-calculus that extends second-order IMLL2, i.e., intuitionistic multiplicative Linear Logic, by means of logical rules that weaken and contract assumptions, but in a purely linear setting. LEM enjoys both a mildly weakened cut-elimination, whose computational cost is cubic, and Subject reduction. A translation of LEM into IMLL2 exists such that the derivations of the former can exponentially compress the dimension of the derivations in the latter. LEM allows for a modular and compact representation of boolean circuits, directly encoding the fan-out nodes, by means of contraction, and disposing garbage, by means of weakening. It can also represent natural numbers with terms very close to standard Church numerals which, moreover, apply to Hereditarily Finite Permutations, i.e. a group structure that exists inside the linear λ-calculus.