We present a novel linear $λ$-calculus for Classical Multiplicative Exponential Linear Logic (\MELL) along the lines of the propositions-as-types paradigm. Starting from the standard term assignment for Intuitionistic Multiplicative Linear Logic (IMLL), we observe that if we incorporate linear negation, its involutive nature implies that both $A\multimap B$ and $B^\perp\multimap A^\perp$ should have the same proofs. The introduction of a linear modus tollens rule, stating that from $B^\perp\multimap A^\perp$ and $A$ we may conclude $B$, allows one to recover classical MLL. Furthermore, a term assignment for this elimination rule, {the study of proof normalization in a $λ$-calculus with this elimination rule} prompts us to define the novel notion of contra-substitution $t \{ a \backslash\!\backslash s \}$. Introduced alongside linear substitution, contra-substitution denotes the term that results from "grabbing" the unique occurrence of $a$ in $t$ and "pulling" from it, in order to turn the term $t$ inside out (much like a sock) and then replacing $a$ with $s$. We call the one-sided natural deduction presentation of classical MLL, the $λ_{\rm MLL}$-calculus. Guided by the behavior of contra-substitution in the presence of the exponentials, we extend it to a similar presentation for MELL. We prove that this calculus is sound and complete with respect to MELL and that it satisfies the standard properties of a typed programming language: subject reduction, confluence and strong normalization. Moreover, we show that several well-known term assignments for classical logic can be encoded in $λ_{\rm MLL}$.

翻译：我们提出了一种新颖的线性$λ$-演算，用于经典乘性指数线性逻辑（\MELL），遵循命题作为类型的范式。从直觉主义乘性线性逻辑（IMLL）的标准项指派出发，我们观察到，如果引入线性否定，其对合性质意味着$A\multimap B$和$B^\perp\multimap A^\perp$应当具有相同的证明。引入线性拒取式规则（即从$B^\perp\multimap A^\perp$和$A$可推出$B$），使我们能够恢复经典MLL。此外，为该消去规则设计项指派，以及研究包含此消去规则的$λ$-演算中的证明归一化，促使我们定义了对置换代$t \{ a \backslash\!\backslash s \}$这一新概念。与线性代换一同引入的对置换代，表示通过“抓住”项$t$中$a$的唯一出现并将其“拉出”，从而将项$t$内外翻转（类似于翻转袜子），然后将$a$替换为$s$所得到的项。我们将经典MLL的这种单侧自然演绎表示称为$λ_{\rm MLL}$-演算。基于对置换代在指数算子存在下的行为指导，我们将其扩展为MELL的类似表示。我们证明该演算相对于MELL是可靠且完备的，并满足类型化编程语言的标准性质：主体归约、合流性和强归一性。此外，我们展示了若干经典逻辑中已知的项指派均可在$λ_{\rm MLL}$中编码。