A type-assignment of linear erasure and duplication

Gianluca Curzi, Luca Roversi

We introduce $\mathsf{LEM}$, a type-assignment system for the linear $\lambda$-calculus that extends second-order ${\mathsf{IMLL}}_2$, i.e., intuitionistic multiplicative Linear Logic, by…