<p>There are plenty such typing systems.</p>

<p>Most work is based on the linear/affine typing system introduced
in (1) and generalised in (2). Here are the main works on this subject.
In (3) the typing system ensures a precise match with <a href="https://en.wikipedia.org/wiki/Programming_Computable_Functions" rel="noreferrer">PCF</a> (int its call-by-name variant -- changing to call-by-value is easy).
In (4) the typing system gives a precise interpretation of the
<a href="https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus" rel="noreferrer">simply typed &lambda;-calculus</a>. (5) does the same thing for <a href="https://en.wikipedia.org/wiki/System_F" rel="noreferrer">System F</a>, (6) does the same for the <a href="https://en.wikipedia.org/wiki/Lambda-mu_calculus" rel="noreferrer">&lambda;&mu;-calculus</a>.   </p>

<p>The typing systems in  (3, 4, 5, 6) are precise in the sense that the inhabitants of translations of &lambda;-calculus types
"are processes coming from lambda expressions", at least up to $\simeq$ (weak typed bisimulation). More precisely, if $\alpha$ is a type in the &lambda;-calculus, and $\Gamma = x_1 : \beta_1, ..., x_n : \beta_n$ is a corresponding typing environment, then the processes $P$ that are typable
as </p>

<p>$$
   \vdash P \triangleright x_1 : \overline{\langle\beta_1\rangle}, ..., x_n : \overline{\langle\beta_n\rangle}, u : (\langle\alpha\rangle)^{\uparrow}
$$</p>

<p>are (up to $\simeq$) the translations of &lambda;-terms $M$ with</p>

<p>$$
   \Gamma \vdash M : \alpha   
$$</p>

<p>(Here $\langle \alpha \rangle$ is the translation of a &lambda;-type $\alpha$ into &pi;-types, and 
$\overline{\tau}$ the <em>dualisation</em> of the &pi;-type $\tau$.) The translations
are fully abstract in the sense that</p>

<p>$$
M =_{\beta\eta} N 
\quad\text{iff}\quad
\langle M \rangle_u \simeq \langle N \rangle_u
$$
(Here $\langle M \rangle_u$ is the translation of $M$, located at $u$.) So the embedding is as precise as one can hope for. (NB, I'm skating over some details above, for ease of presentation.)  Note  that the systems in (3, 4, 5, 6) are closely related -- indeed they are in some sense the same system, although this viewpoint has not yet been published.</p>

<p>If you want a brief summary of how those typing systems ensure confluence, then it is this: they ensure that there is always at most one active output (i.e. an output not under a prefix). This is brutal/syntactic.</p>

<p>Session types (7, 8) can also be used for this purpose, but the
correspondence is not that precise, in parts because session
types are not as constraining as the types deriving
from (1). See (9) as an example where sessions are used to model
<a href="https://en.wikipedia.org/wiki/Effect_system" rel="noreferrer">effects</a> (such as state) in PCF.</p>

<p>Davide Sangiorgi and others have also worked on this problem,
see (10) for a summary.</p>

<p>Aside: as the question correctly guesses, &lambda;-calculus can be seen as an especially well-behaved form of message passing, a viewpoint  put forward 1976 in Carl Hewitt's pioneering work (11) in the  actors tradition. The typing systems above essentially constrain &pi;-calculus so only this well-behaved  message passing is typable. Coincidentally, Milner invented the &pi;-calculus in parts to give a formal model of actors. In hindsight, as (12) explains nicely, there is a small mismatch between actors and &pi;-calculi.</p>

<p><hr>
<sub></p>

<ol>
<li><p>K. Honda, V. Vasconcelos, N. Yoshida: Secure Information Flow
as Typed Process Behaviour.</p></li>
<li><p>K. Honda, N. Yoshida, A uniform type structure for secure information flow.</p></li>
<li><p>M. Berger, K. Honda, N. Yoshida: Sequentiality and the Pi-Calculus</p></li>
<li><p>N. Yoshida, K. Honda, M. Berger: Strong Normalisation in the Pi-Calculus</p></li>
<li><p>M. Berger, K. Honda, N. Yoshida: Genericity and the Pi-Calculus</p></li>
<li><p>K. Honda, N. Yoshida, M. Berger: Control in the Pi-Calculus</p></li>
<li><p>K. Takeuchi, K. Honda, M. Kubo, An Interaction-based Language and its Typing System.</p></li>
<li><p>K. Honda, V. T. Vasconcelos, M. Kubo, Language Primitives and Type Disciplines for Structured Communication-based Programming.</p></li>
<li><p>D. Orchard, N. Yoshida, Effects as sessions, sessions as effects.</p></li>
<li><p>D. Sangiorgi, D. Walker:  The &pi;-Calculus: A Theory of Mobile Processes </p></li>
<li><p>C. Hewitt, Viewing Control Structures as Patterns of Passing Messages.</p></li>
<li><p>S. Fowler, S. Lindley, P. Wadler, Mixing Metaphors: Actors as Channels and Channels as Actors.</p></li>
</ol>

<p></sub></p>

CC BY-SA 3.0
2017-06-14T06:02:19.037Z
Fantastic answer. Now I have a a lot to read up on.
Turion
CC BY-SA 3.0
2017-06-14T07:42:35.680Z
@MartinBerger: One of the major insights I got from your papers (#4 in your list especially) was that linearity wasn't enough to ensure liveness properties. Additionally, we need some way to ensure the causality of communication (ie, that deadlocks arise from cyclic communication dependencies). This is also true for sequential programs (my real interest), but IMO it's harder to understand because what the communication dependencies actually are is either trivial (purely functional programming) or implicit (stateful).
Neel Krishnaswami
CC BY-SA 3.0
2017-06-14T09:12:47.990Z
@Turion Please feel free to contact me if you have more questions.
Martin Berger
CC BY-SA 3.0
2017-06-14T09:17:57.110Z
@NeelKrishnaswami Yes, that's one of the reasons why I believe that computation -- including sequential -- is easier to study as message passing. Coincidentally, the causality tracking in (4) is simple, there is no conceptual problem with tracking more complicated causality. But we were not aware of a lambda-calculus where that is needed.
Martin Berger
CC BY-SA 3.0
2017-06-13T18:50:07.170Z
2017-06-13T19:45:36.003Z
2017-06-13T19:45:36.003Z
Martin Berger
<p>Milner embedded $\lambda$-calculus into $\pi$-calculus, showing that the $\pi$-calculus is capable of Turing-complete, deterministic calculation. Since parallel compositions of processes in the $\pi$-calculus typically have several possible non-confluent reductions, so one can use the $\pi$-calculus to model non-deterministic concurrency.</p>

<p>Type systems are used to prove certain desirable behaviour of programs. For example, simply typed lambda terms always terminate to a lambda abstraction value (the calculus is strongly normalising). So it's just natural to wonder whether we can find a good type system for $\pi$-calculus such that some of its processes correspond to deterministic computations.</p>

<p>Is there a type system for the $\pi$-calculus probably with types for processes such that processes under certain types are always confluent? Even more, could there be certain types such that their values are processes coming from lambda expressions, e.g. encoded in one of Milner's encodings?</p>

<type-theory><type-systems><nondeterminism><concurrency><pi-calculus>
Determinism and pi-calculus
Turion
# Determinism and pi-calculus

(Asked by: username_0 on 2017-06-13)

Milner embedded $\lambda$-calculus into $\pi$-calculus, showing that the $\pi$-calculus is capable of Turing-complete, deterministic calculation. Since parallel compositions of processes in the $\pi$-calculus typically have several possible non-confluent reductions, so one can use the $\pi$-calculus to model non-deterministic concurrency.

Type systems are used to prove certain desirable behaviour of programs. For example, simply typed lambda terms always terminate to a lambda abstraction value (the calculus is strongly normalising). So it's just natural to wonder whether we can find a good type system for $\pi$-calculus such that some of its processes correspond to deterministic computations.

Is there a type system for the $\pi$-calculus probably with types for processes such that processes under certain types are always confluent? Even more, could there be certain types such that their values are processes coming from lambda expressions, e.g. encoded in one of Milner's encodings?

**Tags:** type-theory, type-systems, nondeterminism, concurrency, pi-calculus

---

## 1 answers

### Answer by username_1 on 2017-06-13. Score: 7 | Accepted answer

There are plenty such typing systems.

Most work is based on the linear/affine typing system introduced
in (1) and generalised in (2). Here are the main works on this subject.
In (3) the typing system ensures a precise match with [PCF](https://en.wikipedia.org/wiki/Programming_Computable_Functions) (int its call-by-name variant -- changing to call-by-value is easy).
In (4) the typing system gives a precise interpretation of the
[simply typed λ-calculus](https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus). (5) does the same thing for [System F](https://en.wikipedia.org/wiki/System_F), (6) does the same for the [λμ-calculus](https://en.wikipedia.org/wiki/Lambda-mu_calculus).

The typing systems in (3, 4, 5, 6) are precise in the sense that the inhabitants of translations of λ-calculus types
"are processes coming from lambda expressions", at least up to $\simeq$ (weak typed bisimulation). More precisely, if $\alpha$ is a type in the λ-calculus, and $\Gamma = x\_1 : \beta\_1, ..., x\_n : \beta\_n$ is a corresponding typing environment, then the processes $P$ that are typable
as

$$
\vdash P \triangleright x\_1 : \overline{\langle\beta\_1\rangle}, ..., x\_n : \overline{\langle\beta\_n\rangle}, u : (\langle\alpha\rangle)^{\uparrow}
$$

are (up to $\simeq$) the translations of λ-terms $M$ with

$$
\Gamma \vdash M : \alpha
$$

(Here $\langle \alpha \rangle$ is the translation of a λ-type $\alpha$ into π-types, and
$\overline{\tau}$ the *dualisation* of the π-type $\tau$.) The translations
are fully abstract in the sense that

$$
M =\_{\beta\eta} N
\quad\text{iff}\quad
\langle M \rangle\_u \simeq \langle N \rangle\_u
$$
(Here $\langle M \rangle\_u$ is the translation of $M$, located at $u$.) So the embedding is as precise as one can hope for. (NB, I'm skating over some details above, for ease of presentation.) Note that the systems in (3, 4, 5, 6) are closely related -- indeed they are in some sense the same system, although this viewpoint has not yet been published.

If you want a brief summary of how those typing systems ensure confluence, then it is this: they ensure that there is always at most one active output (i.e. an output not under a prefix). This is brutal/syntactic.

Session types (7, 8) can also be used for this purpose, but the
correspondence is not that precise, in parts because session
types are not as constraining as the types deriving
from (1). See (9) as an example where sessions are used to model
[effects](https://en.wikipedia.org/wiki/Effect_system) (such as state) in PCF.

Davide Sangiorgi and others have also worked on this problem,
see (10) for a summary.

Aside: as the question correctly guesses, λ-calculus can be seen as an especially well-behaved form of message passing, a viewpoint put forward 1976 in Carl Hewitt's pioneering work (11) in the actors tradition. The typing systems above essentially constrain π-calculus so only this well-behaved message passing is typable. Coincidentally, Milner invented the π-calculus in parts to give a formal model of actors. In hindsight, as (12) explains nicely, there is a small mismatch between actors and π-calculi.

---

1. K. Honda, V. Vasconcelos, N. Yoshida: Secure Information Flow
   as Typed Process Behaviour.
2. K. Honda, N. Yoshida, A uniform type structure for secure information flow.
3. M. Berger, K. Honda, N. Yoshida: Sequentiality and the Pi-Calculus
4. N. Yoshida, K. Honda, M. Berger: Strong Normalisation in the Pi-Calculus
5. M. Berger, K. Honda, N. Yoshida: Genericity and the Pi-Calculus
6. K. Honda, N. Yoshida, M. Berger: Control in the Pi-Calculus
7. K. Takeuchi, K. Honda, M. Kubo, An Interaction-based Language and its Typing System.
8. K. Honda, V. T. Vasconcelos, M. Kubo, Language Primitives and Type Disciplines for Structured Communication-based Programming.
9. D. Orchard, N. Yoshida, Effects as sessions, sessions as effects.
10. D. Sangiorgi, D. Walker: The π-Calculus: A Theory of Mobile Processes
11. C. Hewitt, Viewing Control Structures as Patterns of Passing Messages.
12. S. Fowler, S. Lindley, P. Wadler, Mixing Metaphors: Actors as Channels and Channels as Actors.

> **Comments:**
> **username_0**: Fantastic answer. Now I have a a lot to read up on.  
> **username_2**: @MartinBerger: One of the major insights I got from your papers (#4 in your list especially) was that linearity wasn't enough to ensure liveness properties. Additionally, we need some way to ensure the causality of communication (ie, that deadlocks arise from cyclic communication dependencies). This is also true for sequential programs (my real interest), but IMO it's harder to understand because what the communication dependencies actually are is either trivial (purely functional programming) or implicit (stateful).  
> **username_1**: @Turion Please feel free to contact me if you have more questions.  
> **username_1**: @NeelKrishnaswami Yes, that's one of the reasons why I believe that computation -- including sequential -- is easier to study as message passing. Coincidentally, the causality tracking in (4) is simple, there is no conceptual problem with tracking more complicated causality. But we were not aware of a lambda-calculus where that is needed.  

---

