**natural deduction** metalanguage, practical foundations

**type theory** (dependent, intensional, observational type theory, homotopy type theory)

**computational trinitarianism** =

**propositions as types** +**programs as proofs** +**relation type theory/category theory**

The *$\pi$-calculus* is a computational model for concurrent processes that communicate messages through named channels. It subsumes λ-calculus.

In the monadic (here meaning: *unary*) $\pi$-calculus, outputs and inputs only send and receive single names, while the polyadic (here meaning: *$n$-ary*) $\pi$-calculus allows outputs of tuples of names and corresponding inputs.

This calculus permits non-confluent reductions by design, as opposed to other process calculi such as the Interactive Lambda Calculus (ILC).

A process is either:

- an inactive process $0$;
- the parallel composition of two processes $P\mid Q$;
- the replication of a process $!P$;
- a restriction $(\nu n)\,P$ (that is the generation of a fresh name only known to $P$);
- prefixed by an input $n(m).P$;
- prefixed by an output $\overline{n}\langle m\rangle.P$.

Sometimes an indeterministic choice operator $+$ is added to the syntax.

- a server that increments the value it receives: $S=!\mathrm{incr}(a,x).\overline{a}\langle x+1\rangle$;
- a client that calls to the $\mathrm{incr}$ server: $C=(\nu a)\bigl(\overline{\mathrm{incr}}\langle a,4\rangle\mid a(y)\bigr)$;
- the final process by composing the server and the client: $S\mid C$.

The central reduction rule of the $\pi$-calculus is the following:

$\overline{n}\langle a\rangle.P\mid n(b).Q\longrightarrow P\mid Q_{a\mapsto b}\,.$

Several attempts have been made to give the $\pi$-calculus typing systems. It is crucial for $\mathrm{HO}\pi$, a higher-order $\pi$-calculus in which messages can be processes themselves.

Simple types are defined by the following grammar:

$T\longrightarrow\sharp\widetilde{T}$

where $\widetilde{T}$ ranges over (possibly empty) tuples of simple types.

Typing contexts? are lists of hypotheses of the form $n:T$ where $n$ is a channel name and $T$ is a simple type.

Simply typed $\pi$-calculus corresponds to a distributed logic?: using a property proven at some place supposes therefore a call to that property under a name. Theorems can be used many times, but lemmas are limited to one use.

Typing | Intuitive signification |
---|---|

$a(x,y).P:p,q\to r$ | Lemma 1. Under hypotheses $p$, $q$, then $r$. |

$\overline{a}\langle M,N\rangle:r$ | Use Lemma 1, knowing that $p$ and $q$, to prove $r$. |

Session types were introduced by Kohei Honda. A session links exactly two subprocesses that interact with each other, and multiple sessions can run simultaneously.

The process $x(n).\overline{x}\langle n+1\rangle.0$ may be given type $x:?\mathsf{int}.!\mathsf{int}.\mathsf{end}$.

Caires and Pfenning 2010 established a correspondence between dual intuitionistic linear logic? (DILL) and session typed $\pi$-calculus. Later on, Wadler 2012 established a correspondence between classical linear logic (CLL) and the same calculus.

The Calculus of Communicating Systems (CCS) is an important predecessor of the π-calculus. It can be seen as a restriction of π in which only a dummy name $w$ is exchanged in communications, and $w$ cannot be used in subject position (Hirschkoff 2003).

- Robin Milner, Joachim Parrow and David Walker,
*A Calculus of Mobile Processes*, Information and Computation,**100**(1992) 1-40. - Peter Sewell,
*Applied $\pi$ – A Brief Tutorial*, (2000) (pdf). - Jeannette M. Wing,
*FAQ on $\pi$-Calculus*, (2002) (pdf). - Daniel Hirschkoff,
*A brief survey of the theory of the $\pi$-calculus*, (2003) (pdf). - Pierre-Louis Curien,
*Introduction to CCS and $pi$-calculus*, (2003) (ps).

On types:

- Kohei Honda,
*Types for dyadic interaction*, 4th International Conference on Concurrency Theory (1993) 509–523. - Noël Bernard,
*Investigating the Logical Aspects of the Pi-calculus*, Schedae Informaticae,**12**(2003) 57-66 (hal-00386109). - Luís Caires and Frank Pfenning,
*Session Types as Intuitionistic Linear Propositions*, 21st International Conference on Concurrency Theory (2010) 222-236 (pdf). - Philip Wadler,
*Propositions as Sessions*(pdf, doi:10.1145/2398856.2364568).

Other process calculi:

- Kevin Liao, Matthew A. Hammer and Andrew Miller,
*ILC: A Calculus for Composable, Computational Cryptography*, Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, (2019) 640-654 (doi:10.1145/3314221.3314607, pdf).

Last revised on March 8, 2024 at 11:21:47. See the history of this page for a list of all contributions to it.