Are you an EPFL student looking for a semester project?
Work with us on data science and visualisation projects, and deploy your project as an app on top of GraphSearch.
Concept
Π-calculus
Summary
In theoretical computer science, the pi-calculus (or pi-calculus) is a process calculus. The pi-calculus allows channel names to be communicated along the channels themselves, and in this way it is able to describe concurrent computations whose network configuration may change during the computation.
The pi-calculus has few terms and is a small, yet expressive language (see ). Functional programs can be encoded into the pi-calculus, and the encoding emphasises the dialogue nature of computation, drawing connections with game semantics. Extensions of the pi-calculus, such as the spi calculus and applied pi, have been successful in reasoning about cryptographic protocols. Beside the original use in describing concurrent systems, the pi-calculus has also been used to reason about business processes and molecular biology.
The pi-calculus belongs to the family of process calculi, mathematical formalisms for describing and analyzing properties of concurrent computation. In fact, the pi-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).
Central to the pi-calculus is the notion of name. The simplicity of the calculus lies in the dual role that names play as communication channels and variables.
The process constructs available in the calculus are the following (a precise definition is given in the following section):
concurrency, written , where and are two processes or threads executed concurrently.
communication, where
input prefixing is a process waiting for a message that was sent on a communication channel named before proceeding as , binding the name received to the name x. Typically, this models either a process expecting a communication from the network or a label c usable only once by a goto c operation.
output prefixing describes that the name is emitted on channel before proceeding as . Typically, this models either sending a message on the network or a goto c operation.
Official source
About this result
This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.