1: \begin{abstract}

2: We introduce  $\mathsf{LEM}$, a type-assignment system for the linear $ \lambda $-calculus that extends second-order 

3: $\mathsf{IMLL}_2$, i.e., intuitionistic multiplicative Linear Logic, by 

4: means of logical rules that weaken and contract assumptions, but in a 

5: purely linear setting. $\mathsf{LEM}$ enjoys both a mildly weakened 

6: cut-elimination, whose computational cost is cubic, and 

7: Subject reduction. A translation of $\mathsf{LEM}$ 

8: into $\mathsf{IMLL}_2$ exists such that the derivations of the former can 

9: exponentially compress the dimension of the derivations in the latter. 

10: $\mathsf{LEM}$ 

11: allows for a modular and compact representation of boolean circuits, directly encoding the fan-out nodes, 

12: by contraction, and disposing 

13: garbage, by weakening.

14: It can also represent natural numbers with terms  very close to

15: standard Church numerals which, moreover, apply to Hereditarily Finite 

16: Permutations, i.e. a group structure that exists inside the linear 

17: $ \lambda $-calculus.

18: \end{abstract}

19: