Editing Process calculus (section)

== Current research ==

Various process calculi have been studied and not all of them fit the paradigm sketched here. The most prominent example may be the [[ambient calculus]]. This is to be expected as process calculi are an active field of study. Currently research on process calculi focuses on the following problems.

* Developing new process calculi for better modeling of computational phenomena.
* Finding well-behaved subcalculi of a given process calculus. This is valuable because (1) most calculi are fairly ''wild'' in the sense that they are rather general and not much can be said about arbitrary processes; and (2) computational applications rarely exhaust the whole of a calculus. Rather they use only processes that are very constrained in form. Constraining the shape of processes is mostly studied by way of [[type system]]s.
* Logics for processes that allow one to reason about (essentially) arbitrary properties of processes, following the ideas of [[Hoare logic]].
* Behavioural theory: what does it mean for two processes to be the same? How can we decide whether two processes are different or not? Can we find representatives for equivalence classes of processes? Generally, processes are considered to be the same if no context, that is other processes running in parallel, can detect a  difference. Unfortunately, making this intuition precise is subtle and mostly yields unwieldy characterisations of equality (which in most cases must also be undecidable, as a consequence of the [[halting problem]]). [[Bisimulation]]s are a technical tool that aids reasoning about process equivalences.
* Expressivity of calculi. Programming experience shows that certain problems are easier to solve in some languages than in others. This phenomenon calls for a more precise characterisation of the expressivity of calculi modeling computation than that afforded by the [[Church–Turing thesis]]. One way of doing this is to consider encodings between two formalisms and see what properties encodings can potentially preserve. The more properties can be preserved, the more expressive the target of the encoding is said to be. For process calculi, the celebrated results are that the synchronous [[π-calculus]] is more expressive than its asynchronous variant, has the same expressive power as the higher-order [[π-calculus]],<ref>{{Cite book|last=Sangiorgi|first=Davide|title=TAPSOFT'93: Theory and Practice of Software Development |chapter=From π-calculus to higher-order π-calculus — and back |date=1993|editor-last=Gaudel|editor-first=M. -C.|editor2-last=Jouannaud|editor2-first=J. -P.|volume=668|series=Lecture Notes in Computer Science|language=en|publisher=Springer Berlin Heidelberg|pages=151–166|doi=10.1007/3-540-56610-4_62|isbn=9783540475989|doi-access=free}}</ref> but is less than the [[ambient calculus]].{{citation needed|date=December 2011}}
* Using process calculus to model biological systems (stochastic π-calculus, BioAmbients, Beta Binders, BioPEPA, Brane calculus). It is thought by some that the [[compositionality]] offered by process-theoretic tools can help biologists to organise their knowledge more formally.