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.

翻译：Craig插值定理在从数理逻辑到计算机科学的广泛领域中具有重要应用。建立插值定理的证明论技术通常遵循一种由前原首先在矢列演算中引入、后经Prawitz调整适用于自然演绎的方法。该结果可强化为考虑证明项的证明相关版本：Čubrić首次在带和类型的简单类型λ演算中建立了这一结果，近期又在线性、经典和直觉主义矢列演算中得以实现。本文基于双向类型化的原理，给出了Čubrić证明相关插值定理的新证明，并在Rocq中完成了形式化。