2026-07-20T10:52:13Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:3675 2024-03-06T10:34:21Z ddc:004 open_access

Cut Reduction in Linear Logic as Asynchronous Session-Typed Communication DeYoung, Henry Caires, Luís Pfenning, Frank Toninho, Bernardo linear logic cut reduction asynchronous pi-calculus session types 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Henry DeYoung and Luís Caires and Frank Pfenning and Bernardo Toninho 2012 Is Part Of LIPIcs, Volume 16, Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL (2012) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2012.228 urn:nbn:de:0030-drops-36753 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.228 eng https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode