{"id":"arxiv/2603.03083","url":"https://arxiv.org/abs/2603.03083","tags":["cs.LO","cs.PL","math.LO"],"score":0,"title":"Bidirectional Interpolation for the Lambda-Calculus: Revisiting and Formalising Craig-Čubrić Interpolation","domain":"cs.LO","source":"arxiv","authors":["Meven Lennon Bertrand","Alexis Saurin"],"reviews":0,"subject":"cs.LO","summary":"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…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-03-03","reactions":{}}