BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.bham.ac.uk//v3//EN
BEGIN:VEVENT
CATEGORIES:Theoretical computer science seminar
SUMMARY:Taylor expansion in linear logic is invertible: A
completeness result - Daniel de Carvalho\, Innopol
is University
DTSTART:20191101T110000Z
DTEND:20191101T120000Z
UID:TALK3990AT
URL:/talk/index/3990
DESCRIPTION:Each Multiplicative Exponential Linear Logic (MELL
) proof-net can be expanded into a differential ne
t\, which is its Taylor expansion. I recently prov
ed that two different MELL proof-nets have two dif
ferent Taylor expansions. A corollary of this theo
rem is a completeness result for MELL: The relatio
nal model is injective for MELL proof-nets\, i.e.
the equality between MELL proof-nets in the relati
onal model is exactly axiomatized by cut-eliminati
on\, which was conjectured twenty years ago. I wil
l mention some consequences: a new proof of conflu
ence\, the canonicity of the Danos-Regnier syntax\
, a notion of principal typing for linear logic\,
the possibility to investigate normalisation by ev
aluation.
LOCATION:Computer Science\, The Sloman Lounge (UG)
CONTACT:Benedikt Ahrens
END:VEVENT
END:VCALENDAR