LIPIcs.CSL.2012.228.pdf
- Filesize: 480 kB
- 15 pages
Document
Cut Reduction in Linear Logic as Asynchronous Session-Typed Communication
Authors
-
Part of:
Volume:
Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL (CSL 2012)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Computer Science Logic (CSL) - License:
Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
- Publication Date: 2012-09-03
Cite AsGet BibTex
Henry DeYoung, Luís Caires, Frank Pfenning, and Bernardo Toninho. Cut Reduction in Linear Logic as Asynchronous Session-Typed Communication. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 228-242, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
https://doi.org/10.4230/LIPIcs.CSL.2012.228
https://doi.org/10.4230/LIPIcs.CSL.2012.228
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.
Keywords
- linear logic
- cut reduction
- asynchronous pi-calculus
- session types
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads