AI 中文总结
研究λ演算的证明逻辑，通过引入一种逻辑，其模态证明项为类型化λ项，能同时推理计算与证明。给出公理系统、自然演绎系统及Curry-Howard解释，还构建相继式演算并证明切割消去，得到归一化结果。
AI 中文摘要
简单类型λ演算是一种计算模型，通过Curry-Howard对应，类型化项对应直觉主义命题逻辑（IPL）的证明。证明逻辑是一种操作模态逻辑，用显式证明项取代标准的框模态，使逻辑能直接推理其公式的证明。标准证明逻辑通过将IPL的希尔伯特式公理证明嵌入为逻辑的证明项来推理IPL的证明。本文引入一种λ演算的证明逻辑，其中模态的证明项正是类型化λ项本身，它能同时推理计算和证明。首先给出该逻辑的公理系统，接着提出自然演绎系统和Curry-Howard解释，还给出Gentzen风格的相继式演算并证明了切割消去，在负片段中得到归一化结果。
英文摘要
The simply typed λ-calculus is a model of computation where typed terms correspond to proofs of intuitionistic propositional logic (IPL) via the Curry-Howard correspondence. Justification logic is an operational modal logic in which the standard box modality is replaced by an explicit proof term, allowing the logic itself to reason directly about proofs of its formulas. Standard justification logics reason about proofs of IPL by embedding Hilbert-style axiomatic proofs of IPL as proof terms of the logic. We instead introduce a justification logic of the λ-calculus, in which the proof terms of the modality are exactly the typed λ-terms themselves: a modal logic that reasons about computation and proof simultaneously, as both notions coincide under the Curry-Howard interpretation. First, we provide an axiomatisation of this logic. We then propose a natural deduction system and a Curry-Howard interpretation, where a formal connection between the term calculus and the proof terms of the logic is provided. To complete the picture, we give a Gentzen-style sequent calculus for which we prove cut-elimination, and consequently obtain a normalisation result by working in the negative fragment.
