双向插值用于λ演算——重新审视并形式化Craig-Čubrić插值
Bidirectional Interpolation for the Lambda-Calculus: Revisiting and Formalising Craig-Čubrić Interpolation
AI总结：
本文通过双向类型原理重新审视并形式化了Craig-Čubrić插值定理，扩展了其在λ演算和序贯演算中的应用。
摘要：
Craig的插值定理在数学逻辑和计算机科学中有广泛应用。证明论技术通常采用Maehara为序贯演算引入的方法，随后被Prawitz适应到自然演绎中。结果可以加强为证明相关的版本，考虑证明项：这首先由Čubrić在单纯类型λ演算中提出，最近在线性、经典和直觉序贯演算中进一步发展。我们通过构建双向类型的原理，给出了Čubrić证明相关的插值定理的新证明，并在Rocq中形式化了该定理。
英文摘要：
Craig's Interpolation theorem has a wide range of applications, from mathematical logic to computer science. Proof-theoretic techniques for establishing interpolation usually follow a method first introduced by Maehara for the Sequent Calculus and then adapted by Prawitz to Natural Deduction. The result can be strengthened to a proof-relevant version, taking proof terms into account: this was first established by Čubrić in the simply-typed lambda-calculus with sums and more recently in linear, classical and intuitionistic sequent calculi. We give a new proof of Čubrić's proof-relevant interpolation theorem by building on principles of bidirectional typing, and formalise it in Rocq.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
