![]() |
![]() |
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 listsVirtual Harmonic Analysis Seminar SoCS PhD Research Training Sessions SERENE SeminarsOther talksTBC Sylow branching coefficients for symmetric groups Ultrafast, all-optical, and highly efficient imaging of molecular chirality Extending the Lax type operator for finite W-algebras Test talk Modelling uncertainty in image analysis. |