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 result

Add 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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on talks.cam from the University of Cambridge.