The relational model is injective for Multiplicative Exponential Linear Logic

2015/02/09 by de Carvalho, Daniel
#03B70 #FOS: Computer and information sciences #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.1502.02404

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.

Related

• The relational model is injective for Multiplicative Exponential Linear\n Logic (without weakenings)
• Relational type-checking for MELL proof-structures. Part 1: Multiplicatives
• Linear Realisability over nets: multiplicatives (long version)
• An infinitary model of linear logic
• On the role of connectivity in Linear Logic proofs