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}$.
Realizability Interpretation and Normalization of Typed Call-by-Need $$λ$$-calculus With Control
我们定义了一个变体的可实现性，其中实现者是一个长期和一个替代对。这个变体允许我们证明一个简单类型的按需调用$$λ$-$calculus with control due to Ariola et al. Indeed, in such call-by-need calculus, substitutions have to be delayed until knowing if an argument is really needed. In a second step, we extend the proof to a call-by-need $$ λ$-演算的规范化，该演算配备了一个等价于经典二阶谓词逻辑的类型系统，代表了向证明按需调用经典二阶算术的规范化迈出的一步，该算术由第二作者引入，以提供依赖选择公理的证明即程序解释。
Soundness and completeness of the cirquent calculus system CL6 for computability logic
可计算性逻辑是可计算性的形式化理论。Japaridze的早期文章“Introduction to Cirquent Calculus and Abstract Resource Semantics”证明了可计算性逻辑的基本片段CL5的可靠性和完备性。本文将这一结果扩展到更具表现力的cirquent演算系统CL6，这是CL5和经典命题逻辑的保守扩展。
