Cut Reduction in Linear Logic as Asynchronous Session-Typed Communication

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

17 Citations (Scopus)

Abstract

Prior work has shown that intuitionistic linear logic can be seen as a session-type discipline for the π-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 π-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 asyn- chronous interpretation, cut reductions correspond to a natural asynchronous buffered session semantics, where each session is allocated a separate communication buffer.
Original languageUnknown
Title of host publicationLeibniz International Proceedings in Informatics (LIPIcs)
Pages228-242
DOIs
Publication statusPublished - 1 Jan 2012
EventComputer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL -
Duration: 1 Jan 2012 → …

Conference

ConferenceComputer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL
Period1/01/12 → …

Cite this