A Classical Linear $\hat{I}»$-Calculus based on Contraposition

Pablo Barenbaum, Eduardo Bonelli, Leopoldo Lerena

We present a novel linear $\hat{I}»$-calculus for Classical Multiplicative Exponential Linear Logic (\MELL) along the lines of the propositions-as-types paradigm. Starting from the stand…