University of Birmingham > Talks@bham > Theoretical computer science seminar > Taylor expansion in linear logic is invertible: A completeness result

## Taylor expansion in linear logic is invertible: A completeness resultAdd to your list(s) Download to your calendar using vCal - Daniel de Carvalho, Innopolis University
- Friday 01 November 2019, 11:00-12:00
- Computer Science, The Sloman Lounge (UG).
If you have a question about this talk, please contact Benedikt Ahrens. Each Multiplicative Exponential Linear Logic (MELL) proof-net can be expanded into a differential net, which is its Taylor expansion. I recently proved that two different MELL proof-nets have two different Taylor expansions. A corollary of this theorem is a completeness result for MELL : The relational model is injective for MELL proof-nets, i.e. the equality between MELL proof-nets in the relational model is exactly axiomatized by cut-elimination, which was conjectured twenty years ago. I will mention some consequences: a new proof of confluence, the canonicity of the Danos-Regnier syntax, a notion of principal typing for linear logic, the possibility to investigate normalisation by evaluation. This talk is part of the Theoretical computer science seminar series. ## This talk is included in these lists:- Computer Science Departmental Series
- Computer Science Distinguished Seminars
- Computer Science, The Sloman Lounge (UG)
- Theoretical computer science seminar
- computer sience
Note that ex-directory lists are not shown. |
## Other listsCargo Seminars on Advanced Materials PIPS - Postgraduate Informal Physics Seminars## Other talksTBC Solar Physics: more to come ! TBC Advancing biomedical photoacoustic imaging using structured light and optical microresonators [Colloquium:] Aperture Fever: The Extremely Large Telescope (Special colloquium): Quantum enhanced superresolution confocal microscopy |