A Classical Linear $\lambda$-Calculus based on Contraposition

Pablo Barenbaum, Eduardo Bonelli, Leopoldo Lerena

We present a novel linear $\lambda$-calculus for Classical Multiplicative Exponential Linear Logic (\MELL) along the lines of the propositions-as-types paradigm. Starting from the standa…