COMBINATORY FORMULATIONS OF CONCURRENT LANGUAGES

We design a system with six Basic Combinators and prove that it is pow erful enough to embed the full asynchronous pi-calculus, including rep lication. Our theory for constructing Combinatory Versions of concurre nt languages is based on a method, used by Quine and Bernays, for the general elimination of variables in linguistic formalisms. Our combina tors are designed to eliminate the requirement of names that are bound by an input prefix. They also eliminate the need for input prefix, ou tput prefix, and the accompanying mechanism of substitution. We define a notion of bisimulation for the combinatory version and show that th e combinatory version preserves the semantics of the original calculus . One of the distinctive features of the approach is that it can be us ed to rework several process algebras in order to derive equivalent co mbinatory versions.