Taylor expansion in linear logic is invertible: A completeness result

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