The relational model is injective for Multiplicative Exponential Linear Logic
Daniel de Carvalho
TL;DR
This paper proves that the relational model precisely captures equivalence of MELL proof-nets through cut-elimination, establishing a completeness result for the model.
Contribution
It demonstrates that the relational model is injective for MELL proof-nets, providing a complete characterization of proof-net equality.
Findings
Relational model is injective for MELL proof-nets.
Equality in the relational model corresponds exactly to cut-elimination.
Provides a completeness result for the relational model in MELL.
Abstract
We prove a completeness result for Multiplicative Exponential Linear Logic (MELL): we show that 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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.