@InProceedings{Interpolation2026,
  author     = {Lennon-Bertrand, Meven and Saurin, Alexis},
  booktitle  = {17th International Conference on Interactive Theorem Proving (ITP 2026)},
  date       = {2026},
  title      = {{Bidirectional Interpolation for the \lambda-Calculus: Revisiting and Formalising Craig-\v{C}ubri\'{c} Interpolation}},
  doi        = {10.4230/LIPIcs.ITP.2026.30},
  editor     = {Komendantskaya, Ekaterina and Nipkow, Tobias},
  isbn       = {978-3-95977-436-9},
  location   = {Dagstuhl, Germany},
  pages      = {30:1--30:21},
  publisher  = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  series     = {Leibniz International Proceedings in Informatics (LIPIcs)},
  volume     = {382},
  annotation = {Keywords: Craig Interpolation, Bidirectional Typing, Typed Lambda Calculus},
  issn       = {1868-8969},
  urn        = {urn:nbn:de:0030-drops-270049},
}