Prior work has shown that intuitionistic linear logic can be seen as asession-type discipline for the pi-calculus, where cut reduction inthe sequent calculus corresponds to synchronous process reduction. Inthis 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 canbe understood through permutations of inference rules that preserveobservational equivalence of closed processes in the synchronous case.We also show that, under this new asynchronous interpretation, cutreductions correspond to a natural asynchronous buffered sessionsemantics, where each session is allocated a separate communicationbuffer.
展开▼
