DROPS

Document

DOI: 10.4230/LIPIcs.CSL.2016.41

The Relational Model Is Injective for Multiplicative Exponential Linear Logic

Authors: Daniel de Carvalho

Published in: LIPIcs, Volume 62, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)

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.

Cite as

Daniel de Carvalho. The Relational Model Is Injective for Multiplicative Exponential Linear Logic. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 41:1-41:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{decarvalho:LIPIcs.CSL.2016.41,
  author =	{de Carvalho, Daniel},
  title =	{{The Relational Model Is Injective for Multiplicative Exponential Linear Logic}},
  booktitle =	{25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
  pages =	{41:1--41:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-022-4},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{62},
  editor =	{Talbot, Jean-Marc and Regnier, Laurent},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.41},
  URN =		{urn:nbn:de:0030-drops-65815},
  doi =		{10.4230/LIPIcs.CSL.2016.41},
  annote =	{Keywords: Linear Logic, Denotational semantics, Proof-nets}
}

Search Results

Documents authored by de Carvalho, Daniel

The Relational Model Is Injective for Multiplicative Exponential Linear Logic

Abstract

Cite as

Thanks for your feedback!

Could not send message