![]() |
![]() |
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
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:
Note that ex-directory lists are not shown. |
Other listsWhat's on in Physics? Bham Talks SERENE Group Seminar SeriesOther talksLife : it’s out there, but what and why ? Quantum Sensing in Space Proofs of Turán's theorem The tragic destiny of Mileva Marić Einstein TBA TBC |