BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//wp-events-plugin.com//7.2.3.1//EN
TZID:Europe/Paris
X-WR-TIMEZONE:Europe/Paris
BEGIN:VEVENT
UID:5099@i2m.univ-amu.fr
DTSTART;TZID=Europe/Paris:20240328T110000
DTEND;TZID=Europe/Paris:20240328T123000
DTSTAMP:20260107T152156Z
URL:https://www.i2m.univ-amu.fr/evenements/craig-lyndon-interpolation-as-c
 ut-introduction/
SUMMARY:Alexis Saurin (IRIF): Craig-Lyndon interpolation as cut-introductio
 n
DESCRIPTION:Alexis Saurin: In this talk\, I will present a proof-relevant C
 raig-Lyndon interpolation theorem for first-order LL (linear logic). This 
 interpolation result is proof-relevant in the following sense:\nif π prov
 es A ⊢ B and is cut-free\, then we can find\n(i) a formula C in the comm
 on vocabulary of A and B and\n(ii) two proofs π1 and π2 of A ⊢ C and C
  ⊢ B respectively\, such that Cut(π1\,π2) reduces to π.\nI will then 
 show that the interpolation process can be regarded as a cut-introduction 
 procedure\, synthesizing the interpolation formula.\n\nI will then discuss
  how this result follows in fact straightforwardly from the standard proof
 -theoretic method (Maehara's method) used to prove interpolation in a numb
 er of sequent calculi. I will also discuss the computational interpretatio
 n of the result and in particular recall similar results discovered in the
  early nineties by Cubric\, a student of Michael Makkai\, without receivin
 g significant attention.\n\nThen\, depending on time and interest of the a
 udience\, I will possibly discuss\n(i) similar proof-relevant interpolatio
 n results for intuitionistic and classical logics (ii) how to extend the a
 bove result to (a fragment of) circular proofs of linear logic with least 
 and greatest fixed-points and/or\n(iii) a proof-net reformulation of the a
 bove results.
CATEGORIES:Séminaire,Logique et Interactions
LOCATION:I2M Luminy - TPR2\, Salle de Séminaire 304-306 (3ème étage)\, 1
 63 Avenue de Luminy\, Marseille\, 13009\, France
X-APPLE-STRUCTURED-LOCATION;VALUE=URI;X-ADDRESS=163 Avenue de Luminy\, Mars
 eille\, 13009\, France;X-APPLE-RADIUS=100;X-TITLE=I2M Luminy - TPR2\, Sall
 e de Séminaire 304-306 (3ème étage):geo:0,0
END:VEVENT
BEGIN:VTIMEZONE
TZID:Europe/Paris
X-LIC-LOCATION:Europe/Paris
BEGIN:STANDARD
DTSTART:20231029T020000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
END:STANDARD
END:VTIMEZONE
END:VCALENDAR