I initially prepared the following bibliography as a reference for a short course on mobile processes I gave at University of Lisboa. I have made a minor revision to the original bibliography so that it is now, at least in its form, addressed to the general public. I must note that this bibliography is far from comprehensive: my original intension is to offer a smooth introduction to the topic rather than to pursue academic fairness and comprehensiveness. Even as such, there are many topics and references I would like to add to the present list. However any substantial revision of the list may take a long time. Believing such a bibliography may not be useless as a reference for those new to the field, especially to capture its overall landscape, and considering a comprehensive bibliography with a different aim than the present one will compensate it in due time, I decided to make this list public in the present form. If you have any comments on the bibliography (including bugs, accusation on omittance or anything), please e-mail me at: kohei@dcs.ed.ac.uk.
For the compilation of this bibliography, my warm thanks go to the attendants of a short lecture series I gave in Lisbon, for whom the original bibliography was written, to Vasco Vasconcelos who organised the lecture series itself, and to Uwe Nestmann without whom the work would never have been completed. Benjamin Pierce, Uwe and Vasco provided useful comments for which I am grateful. Of course the full responsibility for this bibliography, including comments, selection and possible errors, lies solely in myself.
Before beginning the bibliography, let me list some of the introductory books on (non-mobile) process calculi. These are not necessary for reading the listed papers if one has the basic knowledge on the pi-calculus, which may be gained by reading one of the first three basic references on pi-calculus we shall later list. Among the following books, the book on the calculus CCS offers a technical background on various study on pi-calculus. This is because CCS can be considered as a pi-calculus without name passing, even though the formulation is somewhat different.
Baeton and Wejland, Process Algebra, Cambridge University Press.
Hennessy, Algebraic Theory of Processes, MIT Press.
Hoare, Communicating Sequential Processes, Prentice-Hall.
Milner, Communication and Concurrency, Prentice-Hall.
We now move to papers on mobile processes. There is already a vast body of literature on mobile processes, of which we can introduce only a few. We shall proceed in the following way. First, we select five "basic" references. Even though titled "basic", you do not have to read all of them, but to have them at your side may not be a bad idea. After introducing them, I give a selected list of papers for each specific genre with commentaries. There are certainly other interesting papers, and some genres are clearly missing (we mention such genres at the end), so please remember that this is just those which immediately occurred to me as a good introductory material: the list is far from complete, but may still serve as a useful hint for the concerned topics. The papers are basically given together with their ftp (or http) address if I could find it.
For a comprehensive electronic list of bibliography on pi-calculus, please see the Bibliography on Mobile Processes and the Pi-Calculus, http://liinwww.ira.uka.de/bibliography/Theory/pi.html .
Robin Milner, Functions as Processes. Mathematical Structure in Computer Science 2(2), pp.119--146, 1992. (First appeared in 1990 in ICALP, which is shorter).Next, the original pi-calculus paper cannot be missed as a reference and is still worth taking a close look. It is divided into two parts, and the first part gives an intuitive treatment of the basic ideas, including good examples and discussions. The transition relation which is primarily treated in this paper is the "late" transition relation, which is a little different from the "early" transition relation which is currently most widely in use, though the latter is also presented in this classical treatise too. We note that the late transition is also in use in various places (for one thing it is easier for axiomatisation).
Milner, R., Parrow, J. and Walker, D. A calculus of mobile processes. Part I and II.Another good source, which is indeed intended as an introductory text to pi-calculus, is Milner's own "tutorial" on the polyadic pi-calculus ("polyadic" here denotes that a process can send a sequence of names rather than a single name, the latter being called "monadic"): some parts may not be easy to read, but at any rate a very strong introduction, and is worth reading. In particular it contains the original form of "sorting", the types for pi-calculus based on the usage of names.
Information and Computation, 100(1), 1992. (First appeared in 1989 as a LFCS report).
Robin Milner. Polyadic Pi-Calculus: a tutorial. Proceedings of the International Summer School on Logic Algebra of Specification, Springer Verlag, 1992.The following gives a good and short introduction to pi-calculus as a basic calculus for concurrent computation juxtaposing it with lambda-calculus as a basic calculus for functional computation. Introductions of both calculi capture essential points of these formalisms concisely and effectively. The article is instructive by showing both similarity and difference between two formalisms.
Available at ftp://ftp.cl.cam.ac.uk/users/rm135/ppi.ps.Z .
Benjamin Pierce. Foundational Calculi for Programming Languages. CRC Handbook of Computer Science and Engineering. 1995.Finally, a good (and currently essentially the only) source for a historical account is Milner's Turing Award Lecture, which discusses what led Milner to the introduction of CCS and pi-calculus (the latter done with his co-authors), including the philosophical backgrounds.
Available at http://www.cs.indiana.edu/hyplan/pierce/ftp/crchandbook.ps.gz .
Robin Milner. Elements of Interaction. Communication of ACM, January 1993.
Milner, R. Elements of Interaction. Communication of ACM, January 1993.I already quoted this exposition: it is a good introduction to the overall idea.
Other than those papers quoted in the "must" section, I add a few papers which present the basic notions, or tools, which are used for the study of mobile processes. Such tools include transition relation and bisimilarities (the nut-shell being introduced in the paper by Milner-Parrow-Walker above), structural equality and reduction (presented in Milner's "Functions as Processes" above), equational theories (again the core theory was introduced in the original paper by Milner-Parrow-Walker), modal logics, and types. For modal logics, the original treatise can be found in the following paper.
Milner, R., Parrow, J., and Walker, D. Modal Logics for Mobile Processes. Theoretical Computer Science, Vol. 114, pp. 149-171, 1993.Another is a basic treatment on equational theories (for the strong case).
Joachim Parrow and Davide Sangiorgi. Algebraic Theories for Name-Passing Calculi. Journal of Information and Computation, 120(2), pp. 174-197, 1995.The following paper gives the treatment of bisimulations based on so-called "symbolic bisimulation", which is different from the usual formulation but is useful for proof methods and such, because equations on names are treated explicitly. Huimin Lin did the same thing around the same time. Davide Sangiorgi's "open bisimulation" is also in close relationship (see his http directory mentioned later).
Available at http://www.inria.fr/meije/personnel/Davide.Sangiorgi/mypapers.html .
Michele Boreale and Rocco De Nicola. A Symbolic Semantics for the Pi-Calculus. CONCUR'94, 5th Intl. Conference on Concurrency Theory, Lecture Notes in Computer Science, Vol. 836, pp. 299-314, Springer-Verlag, 1994.One may also be interested in how equivalences other than bisimilarity arise in the present setting. The following paper shows a treatment of testing equivalence, by the same authors as the preceding paper. This would offer a reference point from which various non-bisimulation equivalence can be developed.
Michele Boreale and Rocco De Nicola. Testing equivalence for mobile processes. CONCUR'92, 3rd Intl. Conference on Concurrency Theory, Lecture Notes in Computer Science, Vol. 630, pp. 2-16, Springer-Verlag, 1994.Finally the following two papers treat yet another way of defining process equivalence, i.e. the ways based on reduction relation (actually these two give two distinct notions of reduction-based bisimulations). The conception of using reduction for semantics was around the same time, in 1991.
Robin Milner and Davide Sangiorgi. Barbed Bisimulation. Proc. of 19th International Colloquium on Automata, Languages and Programming (ICALP '92), Lecture Notes in Computer Science, Vol. 623, pp. 685-695, Springer-Verlag, 1992.
Available at http://www.inria.fr/meije/personnel/Davide.Sangiorgi/mypapers.html .
Kohei Honda and Nobuko Yoshida. On Reduction-Based Process Semantics. Theoretical Computer Science, 152(2), pp. 437-486, 1995. (a short version as FSTTCS'13, LNCS 761, pp. 373--387, Springer-Verlag, December 1993).Other basic tools to study mobile processes are non-interleaving semantics and types. These are discussed in a later part of this bibliography.
Available at ftp://ftp.dcs.ed.ac.uk/export/kohei/red-sem.ps.gz .
One of the fundamental aspects of pi-calculi is that they offer a common framework into which various computational and communication structures can be represented. Indeed this is one of the foremost appeals of the pi-calculus, and suggests its distinct status among the family of computational calculi. The following work, already quoted, is a primary reference in this context, which shows the encoding of lambda-calculi into pi-calculi. It offers a basic paradigm of the study of such encodings.
Milner, R. Functions as Processes. Mathematical Structure in Computer Science 2(2), pp.119--146, 1992.The next one, which is another basic work in the study of pi-calculus in general and which is worth consulting by everybody, shows an encoding of a representative concurrent object-based language POOL in pi-calculus. The content and presentation are authentic and serves as the basic introduction to how various language constructs (not restricted to higher-order functions) are represented in pi-calculus.
David Walker. Objects in the Pi-calculus. Journal of Information and Computation, 116(2), pp. 253-271, 1995. (first appeared in 1991 in TACS'92)The third paper is an important work by Davide Sangiorgi, which is a deep investigation into Milner's encoding of lambda-calculus (given in "Functions as Processes" above cited). If one is ever to study the area of "functions as processes", this is a work which should be consulted following Milner's work (I warn that one may initially need some efforts to get to the core; but efforts are worth making). Among important main results, it shows that the equation on lambda-terms induced by that of the encoding is precisely characterisable by a Boehm-tree like structure known as Longo-trees.
Davide Sangiorgi. The Lazy Lambda Calculus in a Concurrency Scenario. LICS 92, IEEE, 1992.Davide's another paper treats an encoding of the term-passing pi-calculus into the ordinary pi-calculus (which is also the theme of his Ph.D. thesis). It shows in a quite general setting how term passing can be correctly representable by the combination of name passing and replication. The result gives a certain universality property of name passing and is thus important both theoretically and pragmatically.
Available at http://www.inria.fr/meije/personnel/Davide.Sangiorgi/mypapers.html .
Davide Sangiorgi. >From pi-calculus to Higher-Order pi-calculus --- and back. Proceedings of TAPSOFT'93, Lecture Notes in Computer Science, Vol. 668, pp. 151-166, Springer-Verlag, 1993.The notion of encoding also relates to the issue of expressiveness, on which we discuss in Section 5.
Available at http://www.inria.fr/meije/personnel/Davide.Sangiorgi/mypapers.html .
See also his Ph.D.thesis in the same directory.
Pi-calculus is actually a family of calculi, just as lambda-calculus arises as a family of calculi. Each significant instance of this family gives a basic theoretical tool to understand and analyse varied computational phenomena and to develop practical applications on its basis. Among this family, the asynchronous version of the pi-calculus (meaning whose output prefix becomes body-less) has a very simple syntax and interaction rule whose conciseness can be compared to, say, the untyped lambda calculus, while sufficient to express most known computational structures. The bare minimum simplicity, as well as the significance of asynchronous communication in the distributed computing environments, gives this fragment an important status among the family of pi-calculi. The calculus was introduced independently in the following two papers.
Gerard Boudol. Asynchrony and the pi-calculus (Note). Rapport de Recherche, INRIA Sofia-Antipolis, Number 1702, May 1992.
Available ftp://zenon.inria.fr/meije/theorie-par/gbo/asynchrony.ps.gz.
Kohei Honda and Mario Tokoro. An Object Calculus for Asynchronous Communication.It is notable that this calculus induces a new framework of bisimulation, which is often called "asynchronous bisimulation." It is introduced in the second paper above and is further studied in:
Proc. ECOOP'91, LNCS 512, pp.133--147, Springer-Verlag, 1991.
Available at ftp://ftp.dcs.ed.ac.uk/export/kohei/objcal.ps.gz .
Kohei Honda and Mario Tokoro. On Asynchronous Communication Semantics.See also the paper by Amadio, Castellani and Sangiorgi we list later, which gives the basic syntactic treatment of this bisimilarity. Another paper on this calculus, already cited, gives a basic study on the equational theories of asynchronous processes.
Object-Based Concurrent Computing, Lecture Notes in Computer Science, Vol. 612, pp. 21-51, Springer-Verlag, 1992.
Kohei Honda and Nobuko Yoshida. On Reduction-Based Process Semantics.One interesting topic on this calculus is, as in pi-calculus in general, the usage of names. One of the basic aspects of such usage --- polarity in names --- is studied by Odersky in:
Theoretical Computer Science, 152(2), pp. 437-486, 1995.
Available at ftp://ftp.dcs.ed.ac.uk/export/kohei/red-sem.ps.gz .
Martin Odersky, Polarized Name Passing.Another interesting topic on this calculus is the existence of combinatory representation, just as SKI combinators for lambda-calculus. I list three papers. The first one is easier to read than the second one. The second one however treats the idea of expressiveness seriously in the setting of combinators. The third one is based on a completely different notion of combinators than the previous two (following the idea of a logician Bernays), giving analysis of the mechanism of name passing different from the previous two.
FST & TCS'15, LNCS, 1995.
Available at http://wwwipd.ira.uka.de/~odersky/papers.html/#Concurrent .
Kohei Honda and Nobuko Yoshida, Combinatory Representation of Mobile Processes.
Proceedings of 21st ACM Symposium on Principles of Programming Languages, ACM Press, 1994.
Available at ftp://ftp.dcs.ed.ac.uk/export/kohei/OLD/popl94.ps.gz .
Kohei Honda and Nobuko Yoshida. Replication in Concurrent Combinators.
Proceedings of TACS'94, Lecture Notes in Computer Science, Vol. 789, pp. 786-805, Springer-Verlag, 1994.
Available at ftp://ftp.dcs.ed.ac.uk/export/kohei/OLD/tacs94.ps.gz.
N. Raja and R. K. Shyamasundar. Combinatory Formulations of Concurrent Languages. Algorithms, Concurrency and Knowledge (Proceedings of ACSC'95), Lecture Notes in Computer Science, Vol. 1023, pp. 156-170, Springer-Verlag, December 1995.The combinators that the first two treat are closely related to Lafont's interaction net, hence to Linear Logic. I only list two papers by Lafont: other basic references in this line are Girard's papers on Linear Logics (see for example the directory ftp://lmd.univ-mrs.fr/pub/girard/).
Available at http://www.tcs.tifr.res.in/~raja/publications/publications.html .
Yves Lafont. Interaction Nets, POPL'90, 1990.
Yves Lafont. Interaction Combinators. To appear in Information and Computation.Regarding the syntactic reasoning of this calculus and its bisimilarities, the following work by Amadio, Castellani and Sangiorgi is a basic exposition which presents a few different characterisations of the asynchronous bisimilarities (including the one whose input transitions are restricted to the bound input) and which gives the axiomatisation of the strong asynchronous bisimilarity in the finite setting. All proofs and constructions in the paper are quite refined.
Available at ftp://lmd.univ-mrs.fr/pub/lafont .
Amadio R., Castellani, I, and Sangiorgi, D. On bisimulations for the asynchronous pi-calculus. CONCUR 96, SLNCS 1119, Pisa, 1996. To appear in TCS.The equational theory of the above work is partly based on an original idea of axiomatisation presented in the following paper. The axiomatisation comes from a deep insight on the nature of asynchronous interaction which this calculus represents.
Available at http://www.inria.fr/meije/personnel/Davide.Sangiorgi/mypapers.html.
Martin Hansen, Hans Huttel, and Josva Kleist. Bisimulations for Asynchronous Mobile Processes. Proceedings of Tbilisi Symposium on Logic, Language and Computation, 1995.The following paper gives a very interesting application of the asynchronous bisimulation to solve an issue of expressiveness, which is itself a basic result in that context. We later discuss it in Section 5.
Available at http://www.cs.auc.dk/~hans/Publications/pubs.html.
Uwe Nestmann and Benjamin C. Pierce. Decoding Choice Encodings. Proceedings of CONCUR'96 (International Conference on Concurrency Theory), pages 179-194. LNCS 1119. 1996.There are other works on this calculus, some of which are mentioned in Section 5 as well as at the end of this bibliography. It should also be noted that other members of the pi-family own distinct usage and significance in theory and applications: in particular, as a "small" pi-calculus like the asynchronous version, we may mention Sangiorgi's pi-I-calculus. References to this calculus is given in the next section.
Available at http://www.ercim.org/publication/technical_reports/051-abstract.html .
This topic is closely related to the encoding we discussed earlier: here we are in particular concerned with representation of one name passing calculus in another. One of the key interests in such a study is the examination of significance of each basic construct of pi-calculi via the existence/non-existence of the semantically sound encoding.
One of the basic constructs which have been studied extensively is the summation operator (+). The summation has been the basic operator of process calculi. However Milner noted, in "Functions as Processes", that summation may not be always positioned as an indispensable operator in the presence of name passing. Given the difficulty of implementing even guarded summation in spite of its essential position in axiomatisation, the status of summation becomes an interesting subject of study. One of the first basic results in this context is:
Uwe Nestmann and Benjamin C. Pierce. Decoding Choice Encodings (Extended Abstract). Proceedings of CONCUR'96 (International Conference on Concurrency Theory), pages 179-194. LNCS 1119. 1996.This paper shows how input-guarded summation can be representable without them using asynchronous semantics: it also shows, via a little weaker (or generous) bisimulation called coupled simulation, one can have a tighter representation of input-guarded summation. Another work in this context is Palamidessi's splendid result.
Available at http://www.ercim.org/publication/technical_reports/051-abstract.html .
Catuscia Palamidessi. Comparing the expressive power of the Synchronous and the Asynchronous pi-calculus. POPL'97, pages 256--265, ACM, 1997.Here it is shown that there is a definite difference between a calculus with the "mixed" summation (i.e. the summation whose guards can be both input and output) and a calculus without it. The argument uses a certain invariance of symmetry in summation-less systems, which itself is very interesting. Finally a recent work on summation is Uwe Nestmann's clean construction of the encoding of general sums. One may read this work as a basic analysis of the general sum via the primitive operation of (asynchronous) name passing.
Available at http://www.disi.unige.it/person/PalamidessiC/publications.html .
Uwe Nestmann. What Is a `Good' Encoding of Guarded Choice?. Proceedings of EXPRESS'97, Volume 7 of ENTCS, September 1997.Another interesting topic in representability concerns the sub-systems of pi-calculus in which only "bound output", or private name communication, is permitted, introduced by Davide Sangiorgi. He called this kind of name passing "internal mobility" so that the calculus is called pi-I-calculus. Apart from the surprising expressiveness of this restricted form of interaction, one of the basic features of these restricted calculi is the ease of equational treatment of the calculus based on internal mobility, which may as well have pragmatic significance. Internal mobility also relates to games semantics, on which we shall mention briefly later. Below we present two published papers. In particular the first one combines two original papers on the subject (which appeared in TAPSOFT'95 and ICALP'95, respectively) in one volume.
Available at http://www.brics.dk/RS/97/45/index.html .
Davide Sangiorgi. pi-calculus, internal mobility and agent-passing calculi. Theoretical Computer Science 167(2), 1996.
Available at http://www.inria.fr/meije/personnel/Davide.Sangiorgi/mypapers.html
Michael Boreale. On the Expressiveness of Internal Mobility in Name-Passing Calculi. Proc. 7th Conf. on Concurrency Theory (CONCUR'96), Montanari U. and Sassone, V. eds., Lecture Notes in Computer Science 1119:163-178, Springer-Verlag, 1996.Another calculus of interest in the context of expressiveness is the fusion calculus recently introduced by Parrow and Victor. This is closely related to Milner's reformulation of pi-calculi in the context of action structure (on which we discuss later). There are also other interesting papers on expressiveness which are appearing in various conferences. The representability in general is one of the active and interesting subjects of study on which there are still a lot of work to do.
One basic tool for the study of pi-calculi, which also opens the vast possibility of its practical applications, is types, or sorting, for mobile processes. The original work on sortings is by Milner.
Robin Milner, Polyadic pi-Calculus: a tutorial. Proceedings of the International Summer School on Logic Algebra of Specification, Springer Verlag.The notion of sorting is essentially about how a name is used in processes: in particular what Milner treated in the above paper is the structure of how each name carries another name. The paper treated such sorting in a simplest possible form, though with recursion (i.e. that which allows an output to $a$ carrying a name $a$). The study of the type inference algorithm of the above mentioned simple sorting system is first done by Simon Gay in:
Available at ftp://ftp.cl.cam.ac.uk/users/rm135/ppi.ps.Z .
Simon J. Gay. A Sort Inference Algorithm for the Polyadic pi-Calculus. Proceedings of 20th ACM Symposium on Principles of Programming Languages, ACM Press, 1993.Independently Vasco Vasconcelos and I did a closely related work, which gives a typing system a la Damas-Milner together with an efficient typing algorithm.
Available at http://theory.doc.ic.ac.uk/theory/papers/Gay/sorting.ps.gz .
Vasco Vasconcelos and Kohei Honda. Principal typing schemes in a polyadic pi-calculus. CONCUR'93, 4th Intl. Conference on Concurrency Theory, Lecture Notes in Computer Science, Vol. 715, pp. 524-538, Springer-Verlag, 1993.The following paper by Pierce and Sangiorgi, again done concurrently with and independently from the above two works, treats an important refinement of sorting, which incorporates the input/output mode of name usage in communication. Actually it not only incorporates input/output mode but also treats a refinement by subsorting (whose basic idea is, intuitively: "a process can always behave more stringently than specified by the type"). The subsorting is a sophisticated idea and has an important consequence in behavioural equivalences. The proofs of the main results would be worth consulting for the deep appreciation of the relationship between types and the induced behavioural equivalence (of which this paper presented the initial non-trivial instance).
Available at http://www.di.fc.ul.pt:80/~vv/publications.html .
Benjamin Pierce and Davide Sangiorgi, Typing and Subtyping for Mobile Processes. LICS'93, July 1993.Again independently and concurrently, Turner considered an impredicative polymorphism in sorting, arriving at the encoding of System F in polymorphic pi-calculus, which is later compiled as his Ph.D. thesis. The thesis also treats clean and efficient abstract machine for pi-calculus, which we shall mention later.
Available at http://www.cs.indiana.edu/hyplan/pierce/pierce/ftp/index.html.
David N. Turner. The Polymorphic Pi-Calculus: Theory and Implementation. PhD Thesis, Edinburgh University, 1995.A simpler form of polymorphism, treatable in ML-like type inference, is presented in:
Available at http://www.dcs.gla.ac.uk/~dnt/thesis.ps.gz .
Vasco T. Vasconcelos. Predicative Polymorphism in pi-Calculus. PARLE'94 Parallel Architectures and Languages Europe, Lecture Notes in Computer Science, Vol. 817, pp. 425-437, Springer-Verlag, July 1994.Types in interaction become inherently symmetric (which do relate to the symmetry of formulae in classical linear logic), especially when branching structures are involved. This aspect may have been first studied in:
Available at http://www.di.fc.ul.pt:80/~vv/publications.html .
Kohei Honda. Types for Dyadic Interaction. CONCUR'93, Lecture Notes in Computer Science, 1993, 715, pp.509-523.We finally list a few recent works. There are other works, but these are something which occur to me promptly. The first one treats the linear usage of names (interaction on that name can be done at most once) with emphasis on induced behavioural equivalence.
Available at ftp://ftp.dcs.ed.ac.uk/export/kohei/OLD/concur93a.ps.gz .
Kobayashi, N., Pierce, B. and Turner, D. Linearity and the Pi-Calculus. POPL'96.The second one gives a somewhat general framework of types for processes as a certain partial algebra, which includes the linearity, and show how the mobility can be introduced to the picture.
Available at http://www.cs.indiana.edu/hyplan/pierce/pierce/ftp/index.html .
Kohei Honda. Composing Processes. POPL'96 (POPL), January 1996, pp.344-357.The third one is a basic study on the relationship between types and behavioural equivalence, introducing a strong typing system on monadic pi-calculus and using it to solve an open question in semantics of pi-calculi.
Available at ftp://ftp.dcs.ed.ac.uk/export/kohei/OLD/popl96.ps.gz .
Nobuko Yoshida. Graph Types for Mobile Processes. FSTTCS'16, LNCS 1180, pp.344-357, 1996.The fourth one introduces a somewhat complex typing system based on tags and an ordering relation, with a certain similarity to the above mentioned work by Yoshida, though with more practical aims.
Also as a LFCS Technical Report, ECS-LFCS-96-350, Edinbugh University, 1996.
Available at ftp://ftp.dcs.ed.ac.uk/export/ny/graph1.ps.gz .
Naoki Kobayashi, A Partially Deadlock-free Typed Process Calculus. LICS'97, pp. 128-139, 1997.The final one, a lucidly written recent paper by Pierce and Sangiorgi, studies how (existential) polymorphism in the present setting can and cannot be used for information hiding. Not only the theory itself but also the presented examples are quite interesting, addressing basic aspects of the usage of types in name passing interaction.
Benjamin C. Pierce and Davide Sangiorgi. Behavioural Equivalence in the Polymorphic Pi-Calculus. POPL '97, 1997.More recently Davide Sangiorgi introduced a typing system for a property called "uniform receptiveness" in ICALP'97. Another recent work is by Boudol who studied a notion of types in the setting of blue calculus (see a reference in Section 8). There should be other works but either I do not remember or do not know. Finally I should note that there does not exist a comprehensive framework to treat all of these typing systems, though my treatment in "Composing Processes" tries to do this to some extent. Surely there are a lot of works to be done in this field, and many would be appearing from now on.
Available at http://www.cs.indiana.edu/hyplan/pierce/pierce/ftp/index.html/polybisim.ps.gz .
There are a couple of programming languages based on pi-calculi, on which we list a few conspicuous ones. We first treat Pict, which is the first complete "programming language" based on pi-calculus (in the sense that it has manuals, compilers and such), and has been studied most intensely so far. The core language is essentially the polyadic asynchronous pi-calculus without summation. On the top of this core language, it incorporates various sorting disciplines which have been studied so far by Pierce and his colleagues as well as a few useful shorthand notations, as basic elements of the language. Its implementation is based on Turner's abstract machine introduced in his Ph.D. thesis. For distribution see http://www.cs.indiana.edu/hyplan/pierce/ftp/pict/Html/Pict.html , the home page of Pict.
We list three papers on Pict. The first paper gives several interesting programming examples. The second paper gives a short but illuminating introduction to the design of Pict as a programming language. It is lucidly written and is highly recommended. The third one is a general introduction to the programming in Pict, associated with the public release of the distribution.
Benjamin C. Pierce and David N. Turner. Concurrent Objects in a Process Calculus. Theory and Practice of Parallel Programming (TPPP), Sendai, Japan, Nov. 1994. Springer LNCS, 1995.
Available at http://www.cs.indiana.edu/hyplan/pierce/pierce/ftp/index.html.
Benjamin C. Pierce and David N. Turner. Pict: A Programming Language Based on the Pi-Calculus. 1997, Computer Science Department, Indiana University, To appear in Milner Festschrift, MIT Press, 1997.
Available at http://www.cs.indiana.edu/hyplan/pierce/pierce/ftp/index.html .
Benjamin C.Pierce. Programming in Pi-Calculus: A Tutorial Introduction to Pict.We note that one of the important aims in the study of Pict as an experimental concurrent language is the investigation as to how we can exploit the rich accumulation of the study of types in functional calculi in the present setting. This is clearly an important topic, and the study on and around Pict accumulates various experiences in this regard. What is interesting here would be not only how we can exploit the ideas in typed functional programming effectively in the new setting, but also whether significant new ideas of types which are proper to programming for (mobile) processes arise or not, distinctly from the extant functional notions. But the latter aspect may not be yet evident at the present moment.
Available at http://www.cs.indiana.edu/hyplan/pierce/ftp/pict/pict-4.0/Doc/tutorial.ps.gz .
Another language which is implemented and distributed, and which is again based on asynchronous communication, is designed by Jean-Juc Levy and his group, called Join Calculus. Its core calculus differs from the usual presentation of pi-calculi in that recursion and name passing are combined to form a single operation. One of the emphasis of this project lies in the treatment of locality, distribution and failures, all being essential aspects of distributed programming. For distribution see http://pauillac.inria.fr/join , the home page of join calculus. In the following we list two basic papers. For more introduction see the above mentioned home page.
Cedric Fournet, Georges Gonthier, Jean-Jacques Levy, Luc Maranget and Didier Remy. A calculus of mobile agents. CONCUR'96. In the above mentioned directory.
Cedric Fournet and Georges Gonthier. The reflexive chemical abstract machine and the join-calculus. POPL'96. In the above mentioned directory.Another asynchronous language called TyCO is introduced by Vasco Vasconcelos and has been studied by him and his students. One of the basic difference of the language from Pict and Join Calculus is that it has an embedded branching structure in it, quite like method invocation in concurrent object-oriented programming languages. Again the type discipline is an important element of the language. An implementation exists, but the distribution has not been done yet. The basic introduction of the language can be found in the following paper. There have been a few works concerning TyCO, for which the reader can see Vasco's home page .
Vasco Vasconcelos. Typed concurrent objects. In 8th European Conference on Object-Oriented Programming, volume 821 of LNCS, Pages 100-117. Springer-Verlag, 1994.Finally the following two papers are not so much about a specific language design but rather on a set of structuring constructs for communication-based programming which are born through the examination of pi-calculus encoding of various computational structures. Again a type discipline plays an important role. The first one is an original presentation while the second one gives a definitive version incorporating recursion.
Available at http://www.di.fc.ul.pt:80/~vv/publications.html . (See also other papers in the directory)
Takeuchi, K., Honda, K. and Kubo, M. An Interaction-based Language and its Typing System. PARLE'94, LNCS 817, pp.398--413, Springer-Verlag, 1994.
Available at ftp://ftp.dcs.ed.ac.uk/export/kohei/OLD/parle94.ps.gz .
Honda, K., Vasco V. and Kubo, M. Language primitives and type discipline for structured communication-based programming. ESOP'98, to appear.Concerning all these works, I should note that it is not yet clear whether these approaches to concurrent programming which are based on pi-calculi would indeed be developed into pragmatically useful practice or not: however they surely pose new and important issues on the general principles of concurrent programming for interacting processes, and I myself believe there are wide possibilities for substantial applications of such approaches.
Available at ftp://ftp.dcs.ed.ac.uk/export/kohei/esop98.ps.gz .
Here I list a few works on other subjects. First I give one application of pi-calculus into a denotational semantics of functional computation. Second I refer to Robin Milner's work on action structures, then list a few related works. Finally we give a few pointers for those important topics which have not been treated so far.
First of all, let me note that "applications" of pi-calculi may not be restricted to language design: another natural application area is the reasoning about mobile systems including protocols (on which we mention a little later). Beyond them, there is a vast realm waiting to be explored. As a work suggesting one such possibility, I list the following work by Hyland and Ong. This is far from the only application: but we can glimpse the power of name passing in representing important computational phenomena, even in the setting of sequential programs. We also note that this usage of pi-calculus is closely related to Davide Sangiorgi's pi-I-calculus which we treated in Section 5.
Hyland, M. and Ong, L. Pi-calculus, dialogue games and PCF. Proceedings of 7th Annual ACM Conference on Functional Programming Languages and Computer Architecture, June 26-28, 1995.Second, Robin Milner has been considering an extension of categorical semantics for functional computation in the concurrency setting, under the name of "action structure". Some of these papers study pi-calculi from a different viewpoint from the usual syntactic framework and, as such, are quite interesting. In particular the type structures imposed by the use of categories give clean and in some sense definite treatment of (manipulation of) linkage, which is the primary element of pi-calculus. I only list two papers in this context. The first one is a basic introduction to the topic and which in particular presents an articulation of the basic dynamic elements of pi-calculi in a uniform framework of action structures. I recommend the paper highly not only for the technical content but also for the general research direction it puts forward. The second paper gives theoretical details of the analysis of pi-calculus in action structure, and presents in particular a graphical presentation of pi-calculus called pi-nets.
Available at ftp://ftp.comlab.ox.ac.uk/pub/Documents/techpapers/Luke.Ong.
Milner, R. Calculi for interaction. Acta Informatica, 33:8, 707--737, November, 1995.
Available at ftp://ftp.cl.cam.ac.uk/users/rm135/ac9.ps.Z .
Robin Milner. Action calculi and the pi-calculus. To appear in the Proceedings of NATO Summer School on Logic and Computation, Springer-Verlag, 1993.Other papers on this topic can also be found in the same directory. We mentioned a graphical presentation of pi-calculus above: another graphical presentation is given by Joachim Parrow under the name of "interaction diagrams" (see http://www.sics.se/~joachim/interdia.ps.Z ). These graphical presentation offers the basic understanding on the computational mechanism of pi-calculus from a different angle than syntax.
Available at ftp://ftp.cl.cam.ac.uk/users/rm135/ap.ps.Z. .
We list a few works on pi-calculus in the frameworks related to action structures. First, the following two works discuss concurrency in general and pi-calculus in particular in the framework of Chemical Abstract Machine, which itself has influenced algebraic treatment of pi-calculus in a significant way. Join Calculus we mentioned above is also being studied using this framework.
Gerald Berry and Gerald Boudol. Chemical Abstract Machines.
Theoretical Computer Science, 96:217--248, 1992.
Gerald Boudol. Some chemical abstract machines. Available at ftp://ftp-sop.inria.fr/meije/theorie-par/gbo/rex.ps.gzAmong these two papers, the first one is the general introduction to the chemical abstract machine. The second one shows how fully asynchronous pi-calculus (corresponding to RPIC in Milner's action structure) is treatable in this framework. Related to action structures and chemical abstract machines, I myself did a work in a similar context. Pi-calculus is a calculus of names and their manipulation, and as such the basic understanding of the mathematics of names would be important for its understanding. A trial in this direction is a theory of symmetries on processes, of which the following is a most recent treatment (Section 5 of the paper gives some discussions on pi-calculus in this setting). "Composing Processes" mentioned above is an application of this theory.
Honda, Process Structures, typescript, 79pp. Submitted for publication.A study of concurrent computation in a categorical framework, which is more closely related to action structures in that both dynamics and statics are treated, has been done by Ugo Montanari and his students. A treatment of (asynchronous) pi-calculus in this framework is given in the following paper. Other papers (not necessarily on pi-calculus) can be found in the same directory.
(initial conference version appeared in TPPP'94, LNCS 907, 1995.)
Available at ftp://ftp.dcs.ed.ac.uk/export/kohei/p-str.ps.gz.
GianLuigi Ferrari and Ugo Montanari. A Tile-Based Coordination View of Asynchronous Pi-Calculus. Mathematical Foundations of Computer Science, LNCS 1295. Available at http://www.di.unipi.it/~ugo/mfcs97.ps.
I conclude this bibliography with short notes on those subjects missing from the present list.
(1) First, an important semantic element of mobile processes which we have not treated yet, is the true concurrency (or causality-based) semantics for mobile processes. As far as I know, Boreale, Degano, Priami and Sangiorgi are people who have contributed to this topic. Two basic notions, subject dependency and object (or link) dependency, the latter being proper to, and is significant in, mobile processes, were presented by Boreale and Sangiorgi (available at http://www.inria.fr/meije/personnel/Davide.Sangiorgi/mypapers.html ), while a comprehensive treatment of elements of true concurrency semantics for pi-calculus was given by Degano and Priami (available at http://arena.sci.univr.it/~priami/wwwpapers/nis.ps.gz ). They use proved transition relation, which gives robust syntactic basis for such discussions (and which relates to early works by Boudol and Castellani). Degano and Priami restricted their attention to late transition while Sangiorgi and Boreale used early transition: however early transition should be treatable in the framework Degano and Priami presented.
(2) Secondly, another important topic which I have not mentioned is the further study on modal logics and proof system for mobile processes (including a model checker). This line of study can have an important practical consequence for e.g. program verification, as well as presenting an interesting semantic aspect of mobility. Mads Dam, among others, did a series of basic works in this genre using modal mu-calculus. See for example ftp://ftp.sics.se/pub/fdt/mfd/mcmpiac.ps.Z . Other people involved are (as far as I know) Robert Amadio, Huimin Lin, Faron Moller, and Björn Victor. In particular the latter two together with Mads Dam and Lars-Henrik Eriksson, developed the mobility workbench (see http://www.docs.uu.se/~victor/mwb.html ).
(3) Thirdly and relatedly, an important use of pi-calculi is the verification of real and prototypical "mobile" systems, i.e. systems whose linkage structures dynamically change. An impressive piece of work is a reasoning about (part of) a real-world mobile protocol by Fredrik Orava and Joachim Parrow (see http://www.sics.se/~joachim/handover.ps.Z ), which is worth consulting if one is interested in how pi-calculus helps us to articulate and reason about realistic systems (the work suggests how both aspects are important). As another work in this context, Anna Philippou studied the use of confluence for reasoning about dynamically evolving systems in her Ph.D.thesis under David Walker, with interesting applications. I do not know whether her thesis is electronically available, but a paper by Philippou and Walker in the ICALP'97 proceedings gives a good exposition of a representative case. Another recent use of pi-calculus for verification is a work by Amadio and Prasad (see http://protis.univ-mrs.fr/~amadio/amadio-prasad.ps.gz ): essentially the work gives three abstract models of an Internet protocol with mobile hosts using a variant of asynchronous pi-calculus, and studies behavioural properties of these models. This line of research is also related to extensions of pi-calculus so that it incorporates more realistic features of distributed computing, both at the syntactic level and at the level of types. This line of study is done by (as far as I know) Robert Amadio, Matthew Hennessy, James Riely, Peter Sewell, as well as people working on Join Calculus.
(4) Fourth, Robin Milner's idea of "Functions as Processes" has been extended in a few directions. Among others, Gerald Boudol combined pi-calculus and higher-order functions in his blue calculus (see http://www.inria.fr/meije/personnel/Gerard.Boudol.html ). Joachim Nieren, Gerald Ostheimer, and other people extended Milner's encoding into various strategies, for example to call-by-need lambda-calculi. This line of study is also related to the work by Hyland and Ong mentioned above.
(5) Fifth and finally there are a few works which used domain-theoretic structures to model pi-calculus. These include fully abstract models for May/Must equivalences by Matthew Hennessy as well as two independent and concurrent (though closely related) works by Ian Stark and by Fiore, Moggi and Sangiorgi, both of which appeared in LICS'96.
So this is the end of my list, for the time being. My sincere wish is you will find this topic interesting, and start playing with pi-processes. As I noted, there are a lot of other interesting papers, a lot of other authors who are working on the subject, for whose omission I am responsible: but I hope you can now start from this list to explore those other papers and authors: it is your turn to play the game.
Kohei Honda
Edinburgh University
March 1997/February 1998.