The Buffered Pi-Calculus: A Model for Concurrent Languages
 
         Xiaojie Deng, Yu Zhang, Yuxin Deng and Farong Zhong


Message-passing based concurrent languages are widely used in developing large 
distributed and coordination systems. This paper presents the buffered 
pi-calculus -- a variant of the pi-calculus where channel names are classified 
into buffered and unbuffered: communication along buffered channels is 
asynchronous, and remains synchronous along unbuffered channels. We show that 
the buffered pi-calculus can be fully simulated in the polyadic pi-calculus with 
respect to strong bisimulation. In contrast to the pi-calculus which is hard to 
use in practice, the new language enables easy and clear modeling of practical 
concurrent languages. We encode two real-world concurrent languages in the 
buffered pi-calculus: the (core) Go language and the Core Erlang. Both 
encodings are fully abstract with respect to weak bisimulations.