License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2015.567
URN: urn:nbn:de:0030-drops-54384
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5438/
Go to the corresponding LIPIcs Volume Portal

Breuvart, Flavien ; Pagani, Michele

Modelling Coeffects in the Relational Semantics of Linear Logic

pdf-format:
35.pdf (0.6 MB)

Abstract

Various typing system have been recently introduced giving a parametric version of the exponential modality of linear logic. The parameters are taken from a semi-ring, and allow to express coeffects - i.e. specific requirements of a program with respect to the environment (availability of a resource, some prerequisite of the input, etc.).

We show that all these systems can be interpreted in the relational category (Rel) of sets and relations. This is possible because of the notion of multiplicity semi-ring and allowing a great variety of exponential comonads in Rel. The interpretation of a particular typing system corresponds then to give a suitable notion of stratification of the exponential comonad associated with the semi-ring parametrising the exponential modality.

BibTeX - Entry

@InProceedings{breuvart_et_al:LIPIcs:2015:5438,
  author =	{Flavien Breuvart and Michele Pagani},
  title =	{{Modelling Coeffects in the Relational Semantics of Linear Logic}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{567--581},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-90-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{41},
  editor =	{Stephan Kreutzer},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/5438},
  URN =		{urn:nbn:de:0030-drops-54384},
  doi =		{10.4230/LIPIcs.CSL.2015.567},
  annote =	{Keywords: relational semantics, bounded linear logic, lambda calculus}
}

Keywords: relational semantics, bounded linear logic, lambda calculus
Collection: 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)
Issue Date: 2015
Date of publication: 07.09.2015

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI