Extensions of the π-calculus, such as the spi calculus and applied π, have been successful in reasoning about cryptographic protocols.
Beside the original use in describing concurrent systems, the π-calculus has also been used to reason about business processes[1] and molecular biology.
[2] The π-calculus belongs to the family of process calculi, mathematical formalisms for describing and analyzing properties of concurrent computation.
In fact, the π-calculus, like the λ-calculus, is so minimal that it does not contain primitives such as numbers, booleans, data structures, variables, functions, or even the usual control flow statements (such as if-then-else, while).
The simplicity of the calculus lies in the dual role that names play as communication channels and variables.
In particular, it is easy to define both control structures such as recursion, loops and sequential composition and datatypes such as first-order functions, truth values, lists and integers.
The next step in the process is now Note that since the local name x has been output, the scope of x is extended to cover the third component as well.
After that all concurrently executing processes have stopped Let Χ be a set of objects called names.
This axiom is central, since it describes how a bound name x may be extruded by an output action, causing the scope of x to be extended.
Next, we get the reduction Note that since the local name x has been output, the scope of x is extended to cover the third component as well.
This was first observed by Milner in his paper "Functions as Processes",[10] in which he presents two encodings of the lambda-calculus in the π-calculus.
" – as replicating agents that respond to requests for their bindings by sending back a connection to the term
The features of the π-calculus that make these encodings possible are name-passing and replication (or, equivalently, recursively defined agents).
This can be seen by the fact that bisimulation equivalence becomes decidable for the recursion-free calculus and even for the finite-control π-calculus where the number of parallel components in any process is bounded by a constant.
There are (at least) three different ways of defining labelled bisimulation equivalence in the π-calculus: Early, late and open bisimilarity.
Early and late bisimilarity were both formulated by Milner, Parrow and Walker in their original paper on the π-calculus.
Fortunately, a third definition is possible, which avoids this problem, namely that of open bisimilarity, due to Sangiorgi.
Defining a context as a π term with a hole [] we say that two processes P and Q are barbed congruent, written
In fact, some of the most recent applications lie outside the realm of traditional computer science.
In 1997, Martin Abadi and Andrew Gordon proposed an extension of the π-calculus, the Spi-calculus, as a formal notation for describing and reasoning about cryptographic protocols.
In 2001, Martin Abadi and Cedric Fournet generalised the handling of cryptographic protocols to produce the applied π calculus.
There is now a large body of work devoted to variants of the applied π calculus, including a number of experimental verification tools.
Another example is Cryptyc [3], due to Andrew Gordon and Alan Jeffrey, which uses Woo and Lam's method of correspondence assertions as the basis for type systems that can check for authentication properties of cryptographic protocols.
Around 2002, Howard Smith and Peter Fingar became interested that π-calculus would become a description tool for modeling business processes.
Most recently, the π-calculus has formed the theoretical basis of Business Process Modeling Language (BPML), and of Microsoft's XLANG.
In 1999, Aviv Regev and Ehud Shapiro showed that one can describe a cellular signaling pathway (the so-called RTK/MAPK cascade) and in particular the molecular "lego" which implements these tasks of communication in an extension of the π-calculus.
[2] Following this seminal paper, other authors described the whole metabolic network of a minimal cell.
[15] In 2009, Anthony Nash and Sara Kalvala proposed a π-calculus framework to model the signal transduction that directs Dictyostelium discoideum aggregation.
[16] The π-calculus was originally developed by Robin Milner, Joachim Parrow and David Walker in 1992, based on ideas by Uffe Engberg and Mogens Nielsen.
In his Turing lecture, Milner describes the development of the π-calculus as an attempt to capture the uniformity of values and processes in actors.