2026/01/01 by Meven Lennon-Bertrand, Meven Lennon Bertrand, Alexis Saurin
Computer Science · #Algebra over a field #Bilinear interpolation #Calculus (dental) #Formal Methods in Verification #Interpolation (computer graphics) #Linear interpolation #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Polynomial interpolation #Range (aeronautics) #Sequent #Sequent calculus
paper · pdf · doi:10.4230/lipics.itp.2026.30
openalex publication_date 2026/01/01 · openalex created_date 2026/07/17 · openalex updated_date 2026/07/28
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 λ-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.