Document Open Access Logo

Bidirectional Interpolation for the λ-Calculus: Revisiting and Formalising Craig-Čubrić Interpolation

Authors Meven Lennon-Bertrand , Alexis Saurin

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITP.2026.30.pdf
  • Filesize: 0.81 MB
  • 21 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof theory
  • Theory of computation → Type theory
  • Theory of computation → Type structures
Keywords
  • Craig Interpolation
  • Bidirectional Typing
  • Typed Lambda Calculus

Metrics

Abstract

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.

Cite As Get BibTex

Meven Lennon-Bertrand and Alexis Saurin. Bidirectional Interpolation for the λ-Calculus: Revisiting and Formalising Craig-Čubrić Interpolation. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 30:1-30:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.ITP.2026.30

Author Details

Meven Lennon-Bertrand
  • Université Paris Cité, INRIA, CNRS, IRIF, F-75013 Paris, France
Alexis Saurin
  • Université Paris Cité, CNRS, INRIA, IRIF, F-75013 Paris, France

Funding

The research leading to these results has received funding from the European Research Council (ERC) under the European Union’s Ninth Framework Programme Horizon Europe (ERC Synergy Project Malinca, Grant Agreement n. 101167526).

Supplementary Materials

References

  1. Andreas Abel. Normalization by Evaluation: Dependent Types and Impredicativity. Habilitation thesis, Institut für Informatik, Ludwig-Maximilians-Universität München, 2013. Google Scholar
  2. Andreas Abel and Christian Sattler. Normalization by Evaluation for Call-By-Push-Value and Polarized Lambda Calculus. In Proceedings of the 21st International Symposium on Principles and Practice of Declarative Programming, PPDP ’19, pages 1-12. ACM, October 2019. URL: https://doi.org/10.1145/3354166.3354168.
  3. Henk Barendregt. The Lambda Calculus: Its Syntax and Semantics. Revised Edition. Number 103 in Studies in Logics and the Foundation of Mathematics. North Holland, 1985. Google Scholar
  4. Evert W. Beth. On Padoa’s method in the theory of definition. Indagationes Mathematicae, 15:330-339, 1953. Google Scholar
  5. Sylvain Boulmé. A Proof of Craig’s Interpolation Theorem in Coq. Unpublished, 1996. Google Scholar
  6. Mathis Bouverot-Dupuis, Théo Winterhalter, Kenji Maillard, and Kathrin Stark. Sulfur: Substitution Generation using a Logical Framework. In RocqPL, 2026. Google Scholar
  7. Peter Chapman, James McKinna, and Christian Urban. Mechanising a proof of Craig’s interpolation theorem for intuitionistic logic in Nominal Isabelle. In Serge Autexier, John A. Campbell, Julio Rubio, Volker Sorge, Masakazu Suzuki, and Freek Wiedijk, editors, Intelligent Computer Mathematics, 9th International Conference, AISC 2008, 15th Symposium, Calculemus 2008, 7th International Conference, MKM 2008, Birmingham, UK, July 28 - August 1, 2008. Proceedings, volume 5144 of Lecture Notes in Computer Science, pages 38-52. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-85110-3_5.
  8. Thierry Coquand. An algorithm for type-checking dependent types. Science of Computer Programming, 26(1), 1996. URL: https://doi.org/10.1016/0167-6423(95)00021-6.
  9. William Craig. Linear reasoning. A new form of the Herbrand-Gentzen theorem. J. Symb. Log., 22(3):250-268, 1957. URL: https://doi.org/10.2307/2963593.
  10. William Craig. Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. J. Symb. Log., 22(3):269-285, 1957. URL: https://doi.org/10.2307/2963594.
  11. Pierre-Louis Curien and Hugo Herbelin. The duality of computation. In Proceedings of the fifth ACM SIGPLAN international conference on Functional programming, ICFP00, pages 233-243. ACM, September 2000. URL: https://doi.org/10.1145/351240.351262.
  12. Adrian Dapprich. Generating infrastructural code for terms with binders using MetaCoq and OCaml. Bachelor thesis, Saarland University, 2021. Google Scholar
  13. Nicolaas Govert de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae (Proceedings), 75(5):381-392, 1972. URL: https://doi.org/10.1016/1385-7258(72)90034-0.
  14. Gerard R. Renardel de Lavalette. Interpolation in computing science: the semantics of modularization. Synth., 164(3):437-450, 2008. URL: https://doi.org/10.1007/S11229-008-9358-Y.
  15. Jana Dunfield and Neel Krishnaswami. Bidirectional typing. ACM Computing Surveys, 54(5), 2021. URL: https://doi.org/10.1145/3450952.
  16. Solomon Feferman. Harmonious logic: Craig’s interpolation theorem and its descendants. Synthèse, 164(3):341-357, 2008. URL: https://doi.org/10.1007/S11229-008-9354-2.
  17. Marcelo Fiore. Semantic analysis of normalisation by evaluation for typed lambda calculus. Mathematical Structures in Computer Science, 32(8):1028-1065, 2022. URL: https://doi.org/10.1017/S0960129522000263.
  18. Guido Fiorillo. Proof relevant interpolation and its categorical applications. Master thesis, Université Paris Cité, 2024. Google Scholar
  19. Guido Fiorillo, Daniel Osorio Valencia, and Alexis Saurin. Expanding the realm of Maehara-Čubrić interpolation beyond cut-free, sequent proofs. Unpublished Manuscript, 2025. URL: https://www.irif.fr/_media/users/saurin/pub/draft-int-cut-pn.pdf.
  20. Hugo Férée, Iris van der Giessen, Sam van Gool, and Ian Shillito. Mechanised Uniform Interpolation for Modal Logics K, GL, and iSL, pages 43-60. Springer Nature Switzerland, 2024. URL: https://doi.org/10.1007/978-3-031-63501-4_3.
  21. Hugo Férée and Sam van Gool. Formalizing and computing propositional quantifiers. In Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP ’23, pages 148-158. ACM, January 2023. URL: https://doi.org/10.1145/3573105.3575668.
  22. Jean-Yves Girard. Proof theory and logical complexity, volume 1. Bibliopolis Napoli, 1987. Google Scholar
  23. Jean-Yves Girard, Paul Taylor, and Yves Lafont. Proofs and Types. Cambridge tracts in theoretical computer science. Cambridge University Press, 1989. Google Scholar
  24. Daniel Gratzer, Jonathan Sterling, and Lars Birkedal. Implementing a modal dependent type theory. Proc. ACM Program. Lang., 3(ICFP), 2019. URL: https://doi.org/10.1145/3341711.
  25. Meven Lennon-Bertrand. Complete bidirectional typing for the calculus of inductive constructions. In Liron Cohen and Cezary Kaliszyk, editors, 12th International Conference on Interactive Theorem Proving (ITP 2021), volume 193 of Leibniz International Proceedings in Informatics (LIPIcs). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.ITP.2021.24.
  26. Meven Lennon-Bertrand and Alexis Saurin. Artefact for Bidirectional Interpolation for the Lambda-Calculus. Software, (visited on 2026-07-13). URL: https://github.com/MevenBertrand/interpolation
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.27123
  27. Roger C Lyndon. An interpolation theorem in the predicate calculus. Pacific Journal of Mathematics, 9:129-142, 1959. Google Scholar
  28. Shoji Maehara. On the interpolation theorem of Craig. Sūgaku, 12:235-237, 1960. Google Scholar
  29. Ralph Matthes. Interpolation for natural deduction with generalized eliminations. In Reinhard Kahle, Peter Schroeder-Heister, and Robert Stärk, editors, Proof Theory in Computer Science, pages 153-169, Berlin, Heidelberg, 2001. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/3-540-45504-3_10.
  30. Conor McBride. Types who say ni. Unpublished, 2022. Google Scholar
  31. Kenneth L. McMillan. Interpolation and model checking. In Handbook of Model Checking, pages 421-446. Springer Cham, 2018. URL: https://doi.org/10.1007/978-3-319-10575-8_14.
  32. Julius Michaelis and Tobias Nipkow. Formalized proof systems for propositional logic. In Andreas Abel, Fredrik Nordvall Forsberg, and Ambrus Kaposi, editors, 23rd International Conference on Types for Proofs and Programs (TYPES 2017), volume 104 of Leibniz International Proceedings in Informatics (LIPIcs), pages 5:1-5:16, Dagstuhl, Germany, 2019. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.TYPES.2017.5.
  33. Zanzi Mihejevs and Jules Hedges. Canonical bidirectional typechecking, 2025. URL: https://doi.org/10.48550/arXiv.2512.07511.
  34. Guillaume Munch-Maccagnoni. Syntax and Models of a non-Associative Composition of Programs and Proofs. PhD thesis, Université Paris-Diderot - Paris VII, December 2013. URL: https://theses.hal.science/tel-00918642.
  35. Julian Nagele, Bertram Felgenhauer, and Aart Middeldorp. CSI: New Evidence – A Progress Report, pages 385-397. Springer International Publishing, 2017. URL: https://doi.org/10.1007/978-3-319-63046-5_24.
  36. Frank Pfenning. 15-815 Automated theorem proving. Lecture notes, 1999. URL: https://www.cs.cmu.edu/~fp/courses/99-atp/handouts/intercal.pdf.
  37. Benjamin C. Pierce and David N. Turner. Local type inference. ACM Transactions on Programming Languages and Systems, 22(1):1-44, January 2000. URL: https://doi.org/10.1145/345099.345100.
  38. Andrew M. Pitts. On an interpretation of second order quantification in first order intuitionistic propositional logic. J. Symb. Log., 57(1):33-52, 1992. URL: https://doi.org/10.2307/2275175.
  39. Dag Prawitz. Natural Deduction: A Proof-Theoretical Study. Dover Publications, Mineola, N.Y., 1965. Google Scholar
  40. Tom Ridge. Craig’s interpolation theorem formalised and mechanised in Isabelle/HOL. CoRR, abs/cs/0607058, 2006. URL: https://doi.org/10.48550/arxiv.cs/0607058.
  41. A. Robinson. A result of consistency and its application to the theory of definition. Indagationes Mathematicae, 18, 1956. Google Scholar
  42. Alexis Saurin. Interpolation as Cut-Introduction: On the Computational Content of Craig-Lyndon Interpolation. In Maribel Fernández, editor, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025), volume 337 of Leibniz International Proceedings in Informatics (LIPIcs), pages 32:1-32:21, Dagstuhl, Germany, 2025. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.FSCD.2025.32.
  43. Gabriel Scherer. Deciding equivalence with sums and the empty type. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL ’17, pages 374-386. ACM, January 2017. URL: https://doi.org/10.1145/3009837.3009901.
  44. Kurt Schütte. Proof theory, volume 85. Springer, 1977. Google Scholar
  45. Matthieu Sozeau, Yannick Forster, Meven Lennon-Bertrand, Jakob Nielsen, Nicolas Tabareau, and Théo Winterhalter. Correct and complete type checking and certified erasure for Coq, in Coq. Journal of the ACM, January 2025. URL: https://doi.org/10.1145/3706056.
  46. Matthieu Sozeau and Cyprien Mangin. Equations reloaded: High-level dependently-typed functional programming and proving in Coq. Proc. ACM Program. Lang., 3(ICFP), 2019. URL: https://doi.org/10.1145/3341690.
  47. Kathrin Stark, Steven Schäfer, and Jonas Kaiser. Autosubst 2: reasoning with multi-sorted de Bruijn terms and vector substitutions. In Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP ’19, pages 166-180. ACM, January 2019. URL: https://doi.org/10.1145/3293880.3294101.
  48. William Walker Tait. Intensional interpretations of functionals of finite type I. The journal of symbolic logic, 32(2):198-212, 1967. URL: https://doi.org/10.2307/2271658.
  49. M. Takahashi. Parallel reductions in λ-calculus. Information and Computation, 118(1):120-127, 1995. URL: https://doi.org/10.1006/inco.1995.1057.
  50. Gaisi Takeuti. Proof theory, volume 81. Courier Corporation, 2013. Google Scholar
  51. A. S. Troelstra and H. Schwichtenberg. Basic Proof Theory. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2 edition, 2000. Google Scholar
  52. Jouko A. Väänänen. The Craig interpolation theorem in abstract model theory. Synth., 164(3):401-420, 2008. URL: https://doi.org/10.1007/S11229-008-9357-Z.
  53. Johan van Benthem. The many faces of interpolation. Synth., 164(3):451-460, 2008. URL: https://doi.org/10.1007/S11229-008-9351-5.
  54. Djordje Čubrić. Results in categorical proof theory. PhD thesis, McGill University, 1993. Google Scholar
  55. Djordje Čubrić. Interpolation property for bicartesian closed categories. Archive for Mathematical Logic, 33(4):291-319, August 1994. URL: https://doi.org/10.1007/bf01270628.
  56. Niccolò Veltri and Cheng-Syuan Wan. An Agda formalization of nonassociative lambek calculus and its metatheory. In Gian Luca Pozzato and Tarmo Uustalu, editors, Automated Reasoning with Analytic Tableaux and Related Methods - 34th International Conference, TABLEAUX 2025, Reykjavik, Iceland, September 27-29, 2025, Proceedings, volume 15980 of Lecture Notes in Computer Science, pages 433-452. Springer, 2025. URL: https://doi.org/10.1007/978-3-032-06085-3_23.
  57. Daniel Zackon, Ryan Kavanagh, Alberto Momigliano, and Brigitte Pientka. Rocq CARVe-ing: A library for substructural meta-theory. In RocqPL, 2026. Google Scholar
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact