License
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2012.228
URN: urn:nbn:de:0030-drops-36753
URL: http://drops.dagstuhl.de/opus/volltexte/2012/3675/
Go to the corresponding Portal


DeYoung, Henry ; Caires, Luís ; Pfenning, Frank ; Toninho, Bernardo

Cut Reduction in Linear Logic as Asynchronous Session-Typed Communication

pdf-format:
Document 1.pdf (481 KB)


Abstract

Prior work has shown that intuitionistic linear logic can be seen as a session-type discipline for the pi-calculus, where cut reduction in the sequent calculus corresponds to synchronous process reduction. In this paper, we exhibit a new process assignment from the asynchronous, polyadic pi-calculus to exactly the same proof rules. Proof-theoretically, the difference between these interpretations can be understood through permutations of inference rules that preserve observational equivalence of closed processes in the synchronous case. We also show that, under this new asynchronous interpretation, cut reductions correspond to a natural asynchronous buffered session semantics, where each session is allocated a separate communication buffer.

BibTeX - Entry

@InProceedings{deyoung_et_al:LIPIcs:2012:3675,
  author =	{Henry DeYoung and Lu{\'i}s Caires and Frank Pfenning and Bernardo Toninho},
  title =	{{Cut Reduction in Linear Logic as Asynchronous Session-Typed Communication}},
  booktitle =	{Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
  pages =	{228--242},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-42-2},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{16},
  editor =	{Patrick C{\'e}gielski and Arnaud Durand},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2012/3675},
  URN =		{urn:nbn:de:0030-drops-36753},
  doi =		{http://dx.doi.org/10.4230/LIPIcs.CSL.2012.228},
  annote =	{Keywords: linear logic, cut reduction, asynchronous pi-calculus, session types}
}

Keywords: linear logic, cut reduction, asynchronous pi-calculus, session types
Seminar: Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL
Issue Date: 2012
Date of publication: 27.08.2012


DROPS-Home | Fulltext Search | Imprint Published by LZI