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 -calculus is a computational model for concurrent processes that communicate messages through named channels. It subsumes λ-calculus.
In the monadic (here meaning: unary) -calculus, outputs and inputs only send and receive single names, while the polyadic (here meaning: -ary) -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:
Sometimes an indeterministic choice operator is added to the syntax.
The central reduction rule of the -calculus is the following:
Several attempts have been made to give the -calculus typing systems. It is crucial for , a higher-order -calculus in which messages can be processes themselves.
Simple types are defined by the following grammar:
where ranges over (possibly empty) tuples of simple types.
Typing contexts? are lists of hypotheses of the form where is a channel name and is a simple type.
Simply typed -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 |
---|---|
Lemma 1. Under hypotheses , , then . | |
Use Lemma 1, knowing that and , to prove . |
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 may be given type .
Caires and Pfenning 2010 established a correspondence between dual intuitionistic linear logic? (DILL) and session typed -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 is exchanged in communications, and cannot be used in subject position (Hirschkoff 2003).
On types:
Other process calculi:
Last revised on March 8, 2024 at 11:21:47. See the history of this page for a list of all contributions to it.