A formal language used to specify the actions of processes and their sequential and concurrent composition.  A process calculus has a formal semantics which is useful in attempts to prove certain properties about a software design, such as freedom from DeadLock or LiveLock, or that resources are fairly shared between concurrent processes. See ProofOfCorrectness.

Examples include:
* CSP, CommunicatingSequentialProcesses (http://archive.comlab.ox.ac.uk/csp.html). Also see FiniteStateProcesses.
* CCS (CalculusOfCommunicatingSystems, RobinMilner, TuringAward 1991)
* the PiCalculus (http://www.cs.auc.dk/mobility/)
* the JoinCalculus

''What is the relation between this and the ActionCalculi?''

See http://www.cl.cam.ac.uk/users/rm135/ac9.ps . Essentially, ActionCalculi are descriptions of process calculi (and various other foundational models) using a common mathematical framework.

----
Any reason ActorsModel isn't listed here?  It seems to be sufficiently formal to merit the label "calculus".

''ActorsModel technically isn't a calculus because it (intentionally) is not specified as a notation or language, but rather as a collection of laws that may apply to a given language. So a ProcessCalculus can be an instantiation of the ActorsModel (such as the JoinCalculus, for example).''

----
CategoryConcurrency