The Bufered π-Calculus And Its Application

Message-passing based concurrent languages are widely used in developing largedistributed and coordination systems. This thesis presents the bufered π-calculus—a variant of the π-calculus where channel names are classifed into bufered and un-bufered: communication along bufered channels is asynchronous, and remains syn-chronousalongunbuferedchannels. Weshowthatthebuferedπ-calculuscanbefullysimulated in the polyadic π-calculus with respect to strong bisimulation.In contrast to the π-calculus which is hard to use in practice, the new languageenables easy and clear modeling of practical concurrent languages. We encode tworeal-world concurrent languages in the bufered π-calculus: the (core) Go languageand the Core Erlang. Both encodings are fully abstract w.r.t. weak bisimulations.