伴随自然演绎（扩展版）
Adjoint Natural Deduction (Extended Version)
AI总结：
本文提出伴随逻辑的自然演绎表述，明确其与相继式演算的关联，给出函数式语言形式的计算解释并证明相关计算性质，还提出了精妙的类型检查算法。
摘要：
伴随逻辑是一种组合多种具有不同结构性质的逻辑的通用方法，涵盖线性逻辑、仿射逻辑、严格逻辑以及（普通的）直觉主义逻辑，其中每个命题都具有内在的真之模式。该逻辑此前以相继式演算的形式被定义，因为独立性这一核心概念在该形式下最易被清晰理解，且该形式允许借助标准技术证明切消定理。\n 本文提出了伴随逻辑的一种自然演绎表述，并阐明了它与相继式演算的关联。由此可推导出，每个可证命题都存在一个验证式（有时被称为长范式）。我们还以函数式语言的形式给出了伴随逻辑的一种计算解释，并证明了由模式结构推导而来的计算性质，包括无垃圾性（针对不含弱化和收缩的模式）、严格性（针对不允许弱化的模式）以及可擦除性（基于模式间的预序关系）。最后，我们提出了一种极具精妙性的类型检查算法。
英文摘要：
Adjoint logic is a general approach to combining multiple logics with different structural properties, including linear, affine, strict, and (ordinary) intuitionistic logics, where each proposition has an intrinsic mode of truth. It has been defined in the form of a sequent calculus because the central concept of independence is most clearly understood in this form, and because it permits a proof of cut elimination following standard techniques. In this paper we present a natural deduction formulation of adjoint logic and show how it is related to the sequent calculus. As a consequence, every provable proposition has a verification (sometimes called a long normal form). We also give a computational interpretation of adjoint logic in the form of a functional language and prove properties of computations that derive from the structure of modes, including freedom from garbage (for modes without weakening and contraction), strictness (for modes disallowing weakening), and erasure (based on a preorder between modes). Finally, we present a surprisingly subtle algorithm for type checking.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
