A formalisation of the join-calculus in type theory

Jean-François Monin

Université Joseph Fourier & Verimag Grenoble, France

Work started at France Telecom R&D, with C. Bergerot

Work in progress, including slides

Motivations

Security systems are sensible ▶ hackers like to attack protected systems ▶ the place of attacks are unpredictible ▶ as soon as a flaw is discovered, it will be exploited

as much as possible We cannot afford to rely on security systems which are not completely formally proven correct More realistically : we have to be clear on the precise extent of what is proven

Motivations

Practice of formal methods: 3 potential weaknesses ▶ relevance of the model ▶ complexity ▶ tedious parts

Relevance of the model

The underlying model should rely on assumptions ▶ realistic (close to the real thing) ▶ explicit

Distributed systems

▶ calculi based on a centralized view of the world ▷ CCS, SCP, (basic) π-calculus … ▷ global state transition systems ⇒ distributed consensus

▶ calculi based on local interactions ▷ join-calculus ▷ proof theoretical approaches ⇒ local reasoning

Complexity

Complete formalisation

⇒ everything is explicit

⇒ complexity tends to become unmanageable ▶ basic design decisions are fundamental:

spent time on simplicity and uniformity ▶ support tools e.g. Coq, HOL,…

tedious parts must be checked Useful features: ▶ higher order reasoning ▶ inductive reasoning ▶ reliability of support tools, kernel based (LCF)

Outline

The join-calculus Type theoretical concerns Formalisation in CIC (Calculus of Inductive Constructions) Future work

The Join Calculus

http://pauillac.inria.fr/join/
Fournet, Gonthier, Lévy, Maranget, Rémy

A calculus of mobile processes, like π-calculus ▶ simple: very small number of constructs ▶ less primitive than π-calculus in some sense... ▶ ...but without hidden complexity

(s.t. distributed consensus, uncontrolable scopes) ▷ model closer to real systems ▷ efficient implementations: JC, JoCaml

Several versions ▶ core, asynchronous / synchronous, pure / +constants

Example

def mkcell⟨v_{0}, κ_{0}⟩ ▷

def set⟨u⟩, κ⟩| cell⟨v⟩ ▷ cell⟨u⟩| κ⟨⟩

& get⟨κ⟩ | cell⟨v⟩ ▷ cell⟨v⟩ | κ⟨v⟩

in cell⟨v_{0}⟩ | κ_{0}⟨get, set⟩

in ⟨get_{1}, set_{1}⟩ := mkcell⟨0⟩ ; … set_{1}⟨3⟩ ; … x := get_{1}⟨⟩ ; …

\begin{matrix}s⟨u⟩ | c⟨v⟩ & ▷ c⟨u⟩| κ⟨⟩ \\ g⟨κ⟩ | c⟨v⟩ & ▷ c⟨v⟩ | κ⟨v⟩ \end{matrix}

M ⟨v_{0}, κ_{0}⟩ ▷  c⟨v_{0}⟩  κ_{0}⟨..⟩

\begin{matrix}s_{1}⟨u⟩ | c_{1}⟨v⟩ & ▷ c_{1}⟨u⟩| κ⟨⟩ \\ g_{1}⟨κ⟩ | c_{1}⟨v⟩ & ▷ c_{1}⟨v⟩ | κ⟨v⟩ \end{matrix}

def mkcell⟨v_{0}, κ_{0}⟩ ▷

def set⟨u⟩, κ⟩| cell⟨v⟩ ▷ cell⟨u⟩| κ⟨⟩

& get⟨κ⟩ | cell⟨v⟩ ▷ cell⟨v⟩ | κ⟨v⟩

in cell⟨v_{0}⟩ | κ_{0}⟨get, set⟩

in ⟨get_{1}, set_{1}⟩ := mkcell⟨0⟩ ; … set_{1}⟨3⟩ ; … x := get_{1}⟨⟩ ; …

\begin{matrix}s⟨u⟩ | c⟨v⟩ & ▷ c⟨u⟩| κ⟨⟩ \\ g⟨κ⟩ | c⟨v⟩ & ▷ c⟨v⟩ | κ⟨v⟩ \end{matrix}

M ⟨v_{0}, κ_{0}⟩ ▷  c⟨v_{0}⟩  κ_{0}⟨..⟩

\begin{matrix}s_{1}⟨u⟩ | c_{1}⟨v⟩ & ▷ c_{1}⟨u⟩| κ⟨⟩ \\ g_{1}⟨κ⟩ | c_{1}⟨v⟩ & ▷ c_{1}⟨v⟩ | κ⟨v⟩ \end{matrix}

def mkcell⟨v_{0}, κ_{0}⟩ ▷

def set⟨u⟩, κ⟩| cell⟨v⟩ ▷ cell⟨u⟩| κ⟨⟩

& get⟨κ⟩ | cell⟨v⟩ ▷ cell⟨v⟩ | κ⟨v⟩

in cell⟨v_{0}⟩ | κ_{0}⟨get, set⟩

in ⟨get_{1}, set_{1}⟩ := mkcell⟨0⟩ ; … set_{1}⟨3⟩ ; … x := get_{1}⟨⟩ ; …

\begin{matrix}s⟨u⟩ | c⟨v⟩ & ▷ c⟨u⟩| κ⟨⟩ \\ g⟨κ⟩ | c⟨v⟩ & ▷ c⟨v⟩ | κ⟨v⟩ \end{matrix}

M ⟨v_{0}, κ_{0}⟩ ▷  c⟨v_{0}⟩  κ_{0}⟨..⟩

\begin{matrix}s_{1}⟨u⟩ | c_{1}⟨v⟩ & ▷ c_{1}⟨u⟩| κ⟨⟩ \\ g_{1}⟨κ⟩ | c_{1}⟨v⟩ & ▷ c_{1}⟨v⟩ | κ⟨v⟩ \end{matrix}

def mkcell⟨v_{0}, κ_{0}⟩ ▷

def set⟨u⟩, κ⟩| cell⟨v⟩ ▷ cell⟨u⟩| κ⟨⟩

& get⟨κ⟩ | cell⟨v⟩ ▷ cell⟨v⟩ | κ⟨v⟩

in cell⟨0⟩ | … | get⟨x⟩ | … | set⟨3⟩ | …cell⟨v_{0}⟩ | κ_{0}⟨get, set⟩ in ⟨get_{1}, set_{1}⟩ := mkcell⟨0⟩ ; … set_{1}⟨3⟩ ; … x := get_{1}⟨⟩ ; …

\begin{matrix}s⟨u⟩ | c⟨v⟩ & ▷ c⟨u⟩| κ⟨⟩ \\ g⟨κ⟩ | c⟨v⟩ & ▷ c⟨v⟩ | κ⟨v⟩ \end{matrix}

M ⟨v_{0}, κ_{0}⟩ ▷  c⟨v_{0}⟩  κ_{0}⟨..⟩

\begin{matrix}s_{1}⟨u⟩ | c_{1}⟨v⟩ & ▷ c_{1}⟨u⟩| κ⟨⟩ \\ g_{1}⟨κ⟩ | c_{1}⟨v⟩ & ▷ c_{1}⟨v⟩ | κ⟨v⟩ \end{matrix}

def mkcell⟨v_{0}, κ_{0}⟩ ▷

def set⟨u, κ⟩ | cell⟨v⟩ ▷ cell⟨u⟩ | κ⟨⟩

& get⟨κ⟩ | cell⟨v⟩ ▷ cell⟨v⟩ | κ⟨v⟩

in cell⟨0⟩ | … | get⟨x⟩ | … | set⟨3, d⟩ | …cell⟨v_{0}⟩ | κ_{0}⟨get, set⟩ in ⟨get_{1}, set_{1}⟩ := mkcell⟨0⟩ ; … set_{1}⟨3⟩ ; … x := get_{1}⟨⟩ ; …

\begin{matrix}s⟨u, κ⟩ | c⟨v⟩ & ▷ c⟨u⟩ | κ⟨⟩ \\ g⟨κ⟩ | c⟨v⟩ & ▷ c⟨v⟩ | κ⟨v⟩ \end{matrix}

M ⟨v_{0}, κ_{0}⟩ ▷  c⟨v_{0}⟩  κ_{0}⟨..⟩

\begin{matrix}s_{1}⟨u, κ⟩ | c_{1}⟨v⟩ & ▷ c_{1}⟨u⟩ | κ⟨⟩ \\ g_{1}⟨κ⟩ | c_{1}⟨v⟩ & ▷ c_{1}⟨v⟩ | κ⟨v⟩ \end{matrix}

def mkcell⟨v_{0}, κ_{0}⟩ ▷

def set⟨u, κ⟩ | cell⟨v⟩ ▷ cell⟨u⟩ | κ⟨⟩

& get⟨κ⟩ | cell⟨v⟩ ▷ cell⟨v⟩ | κ⟨v⟩

in cell⟨0⟩ | … x := get⟨⟩ ; … set⟨3⟩; …cell⟨v_{0}⟩ | κ_{0}⟨get, set⟩ in ⟨get_{1}, set_{1}⟩ := mkcell⟨0⟩ ; … set_{1}⟨3⟩ ; … x := get_{1}⟨⟩ ; …

\begin{matrix}s⟨u, κ⟩ | c⟨v⟩ & ▷ c⟨u⟩ | κ⟨⟩ \\ g⟨κ⟩ | c⟨v⟩ & ▷ c⟨v⟩ | κ⟨v⟩ \end{matrix}

M ⟨v_{0}, κ_{0}⟩ ▷  c⟨v_{0}⟩  κ_{0}⟨..⟩

\begin{matrix}s_{1}⟨u, κ⟩ | c_{1}⟨v⟩ & ▷ c_{1}⟨u⟩ | κ⟨⟩ \\ g_{1}⟨κ⟩ | c_{1}⟨v⟩ & ▷ c_{1}⟨v⟩ | κ⟨v⟩ \end{matrix}

def mkcell⟨v_{0}, κ_{0}⟩ ▷

def set⟨u, κ⟩ | cell⟨v⟩ ▷ cell⟨u⟩ | κ⟨⟩

& get⟨κ⟩ | cell⟨v⟩ ▷ cell⟨v⟩ | κ⟨v⟩

in cell⟨v_{0}⟩ | κ_{0}⟨get, set⟩

in ⟨get_{1}, set_{1}⟩ := mkcell⟨0⟩ ; … set_{1}⟨3⟩ ; … x := get_{1}⟨⟩ ; …

M ⟨v_{0}, κ_{0}⟩ ▷  c⟨v_{0}⟩  κ_{0}⟨..⟩

\begin{matrix}s_{1}⟨u, κ⟩ | c_{1}⟨v⟩ & ▷ c_{1}⟨u⟩ | κ⟨⟩ \\ g_{1}⟨κ⟩ | c_{1}⟨v⟩ & ▷ c_{1}⟨v⟩ | κ⟨v⟩ \end{matrix}

def mkcell⟨v_{0}, κ_{0}⟩ ▷

def set⟨u, κ⟩ | cell⟨v⟩ ▷ cell⟨u⟩ | κ⟨⟩

& get⟨κ⟩ | cell⟨v⟩ ▷ cell⟨v⟩ | κ⟨v⟩

in cell⟨v_{0}⟩ | κ_{0}⟨get, set⟩

in ⟨get_{1}, set_{1}⟩ := mkcell⟨0⟩; … set_{1}⟨3⟩; … x := get_{1}⟨⟩; …in ⟨get_{1}, set_{1}⟩ := mkcell⟨0⟩ ; … set_{1}⟨3⟩ ; … x := get_{1}⟨⟩ ; …

M ⟨v_{0}, κ_{0}⟩ ▷  c⟨v_{0}⟩  κ_{0}⟨..⟩

\begin{matrix}s_{1}⟨u, κ⟩ | c_{1}⟨v⟩ & ▷ c_{1}⟨u⟩ | κ⟨⟩ \\ g_{1}⟨κ⟩ | c_{1}⟨v⟩ & ▷ c_{1}⟨v⟩ | κ⟨v⟩ \end{matrix}

def mkcell⟨v_{0}, κ_{0}⟩ ▷

def set⟨u, κ⟩ | cell⟨v⟩ ▷ cell⟨u⟩ | κ⟨⟩

& get⟨κ⟩ | cell⟨v⟩ ▷ cell⟨v⟩ | κ⟨v⟩
in cell⟨v_{0}⟩ | κ_{0}⟨get, set⟩

in ⟨get_{1}, set_{1}⟩ := mkcell⟨0⟩ ; … set_{1}⟨3⟩ ; … x := get_{1}⟨⟩ ; …

M ⟨v_{0}, κ_{0}⟩ ▷  c⟨v_{0}⟩  κ_{0}⟨..⟩  M ⟨0, a⟩

\begin{matrix}s_{1}⟨u, κ⟩ | c_{1}⟨v⟩ & ▷ c_{1}⟨u⟩ | κ⟨⟩ \\ g_{1}⟨κ⟩ | c_{1}⟨v⟩ & ▷ c_{1}⟨v⟩ | κ⟨v⟩ \end{matrix}

def mkcell⟨v_{0}, κ_{0}⟩ ▷

def set⟨u, κ⟩ | cell⟨v⟩ ▷ cell⟨u⟩ | κ⟨⟩

& get⟨κ⟩ | cell⟨v⟩ ▷ cell⟨v⟩ | κ⟨v⟩

in cell⟨v_{0}⟩ | κ_{0}⟨get, set⟩

in ⟨get_{1}, set_{1}⟩ := mkcell⟨0⟩ ; … set_{1}⟨3⟩ ; … x := get_{1}⟨⟩ ; …

M ⟨v_{0}, κ_{0}⟩ ▷  c⟨v_{0}⟩  κ_{0}⟨..⟩

M ⟨0, a⟩

\begin{matrix}s_{1}⟨u, κ⟩ | c_{1}⟨v⟩ & ▷ c_{1}⟨u⟩ | κ⟨⟩ \\ g_{1}⟨κ⟩ | c_{1}⟨v⟩ & ▷ c_{1}⟨v⟩ | κ⟨v⟩ \end{matrix}

def mkcell⟨v_{0}, κ_{0}⟩ ▷

def set⟨u, κ⟩ | cell⟨v⟩ ▷ cell⟨u⟩ | κ⟨⟩

& get⟨κ⟩ | cell⟨v⟩ ▷ cell⟨v⟩ | κ⟨v⟩
in cell⟨v_{0}⟩ | κ_{0}⟨get, set⟩

in ⟨get_{1}, set_{1}⟩ := mkcell⟨0⟩ ; … set_{1}⟨3⟩ ; … x := get_{1}⟨⟩ ; …

M ⟨v_{0}, κ_{0}⟩ ▷  c⟨v_{0}⟩  κ_{0}⟨..⟩

\begin{matrix}s_{1}⟨u, κ⟩ | c_{1}⟨v⟩ & ▷ c_{1}⟨u⟩ | κ⟨⟩ \\ g_{1}⟨κ⟩ | c_{1}⟨v⟩ & ▷ c_{1}⟨v⟩ | κ⟨v⟩ \end{matrix}  a⟨g_{1}, s_{1}⟩

def mkcell⟨v_{0}, κ_{0}⟩ ▷

def set⟨u, κ⟩ | cell⟨v⟩ ▷ cell⟨u⟩ | κ⟨⟩

& get⟨κ⟩ | cell⟨v⟩ ▷ cell⟨v⟩ | κ⟨v⟩

in cell⟨v_{0}⟩ | κ_{0}⟨get, set⟩

in ⟨get_{1}, set_{1}⟩ := mkcell⟨0⟩ ; … set_{1}⟨3⟩ ; … x := get_{1}⟨⟩ ; …

M ⟨v_{0}, κ_{0}⟩ ▷  c⟨v_{0}⟩  κ_{0}⟨..⟩

\begin{matrix}s_{1}⟨u, κ⟩ | c_{1}⟨v⟩ & ▷ c_{1}⟨u⟩ | κ⟨⟩ \\ g_{1}⟨κ⟩ | c_{1}⟨v⟩ & ▷ c_{1}⟨v⟩ | κ⟨v⟩ \end{matrix}

def mkcell⟨v_{0}, κ_{0}⟩ ▷

def set⟨u, κ⟩ | cell⟨v⟩ ▷ cell⟨u⟩ | κ⟨⟩

& get⟨κ⟩ | cell⟨v⟩ ▷ cell⟨v⟩ | κ⟨v⟩

in cell⟨v_{0}⟩ | κ_{0}⟨get, set⟩

in ⟨get_{1}, set_{1}⟩ := mkcell⟨0⟩ ; … set_{1}⟨3⟩ ; … x := get_{1}⟨⟩ ; …

M ⟨v_{0}, κ_{0}⟩ ▷  c⟨v_{0}⟩  κ_{0}⟨..⟩

\begin{matrix}s_{1}⟨u, κ⟩ | c_{1}⟨v⟩ & ▷ c_{1}⟨u⟩ | κ⟨⟩ \\ g_{1}⟨κ⟩ | c_{1}⟨v⟩ & ▷ c_{1}⟨v⟩ | κ⟨v⟩ \end{matrix}  s_{1}⟨3, b⟩

def mkcell⟨v_{0}, κ_{0}⟩ ▷

def set⟨u, κ⟩ | cell⟨v⟩ ▷ cell⟨u⟩ | κ⟨⟩

& get⟨κ⟩ | cell⟨v⟩ ▷ cell⟨v⟩ | κ⟨v⟩

in cell⟨v_{0}⟩ | κ_{0}⟨get, set⟩

in ⟨get_{1}, set_{1}⟩ := mkcell⟨0⟩ ; … set_{1}⟨3⟩ ; … x := get_{1}⟨⟩ ; …

M ⟨v_{0}, κ_{0}⟩ ▷  c⟨v_{0}⟩  κ_{0}⟨..⟩

\begin{matrix}s_{1}⟨u, κ⟩ | c_{1}⟨v⟩ & ▷ c_{1}⟨u⟩ | κ⟨⟩ \\ g_{1}⟨κ⟩ | c_{1}⟨v⟩ & ▷ c_{1}⟨v⟩ | κ⟨v⟩ \end{matrix}  b⟨⟩

def mkcell⟨v_{0}, κ_{0}⟩ ▷

def set⟨u, κ⟩ | cell⟨v⟩ ▷ cell⟨u⟩ | κ⟨⟩

& get⟨κ⟩ | cell⟨v⟩ ▷ cell⟨v⟩ | κ⟨v⟩

in cell⟨v_{0}⟩ | κ_{0}⟨get, set⟩

in ⟨get_{1}, set_{1}⟩ := mkcell⟨0⟩ ; … set_{1}⟨3⟩ ; … x := get_{1}⟨⟩ ; …

M ⟨v_{0}, κ_{0}⟩ ▷  c⟨v_{0}⟩  κ_{0}⟨..⟩

\begin{matrix}s_{1}⟨u, κ⟩ | c_{1}⟨v⟩ & ▷ c_{1}⟨u⟩ | κ⟨⟩ \\ g_{1}⟨κ⟩ | c_{1}⟨v⟩ & ▷ c_{1}⟨v⟩ | κ⟨v⟩ \end{matrix}

def mkcell⟨v_{0}, κ_{0}⟩ ▷

def set⟨u, κ⟩ | cell⟨v⟩ ▷ cell⟨u⟩ | κ⟨⟩

& get⟨κ⟩ | cell⟨v⟩ ▷ cell⟨v⟩ | κ⟨v⟩

in cell⟨v_{0}⟩ | κ_{0}⟨get, set⟩

in ⟨get_{1}, set_{1}⟩ := mkcell⟨0⟩ ; … set_{1}⟨3⟩ ; … x := get_{1}⟨⟩ ; …

M ⟨v_{0}, κ_{0}⟩ ▷  c⟨v_{0}⟩  κ_{0}⟨..⟩

\begin{matrix}s_{1}⟨u, κ⟩ | c_{1}⟨v⟩ & ▷ c_{1}⟨u⟩ | κ⟨⟩ \\ g_{1}⟨κ⟩ | c_{1}⟨v⟩ & ▷ c_{1}⟨v⟩ | κ⟨v⟩ \end{matrix}  g_{1}⟨x⟩

def mkcell⟨v_{0}, κ_{0}⟩ ▷

def set⟨u, κ⟩ | cell⟨v⟩ ▷ cell⟨u⟩ | κ⟨⟩

& get⟨κ⟩ | cell⟨v⟩ ▷ cell⟨v⟩ | κ⟨v⟩

in cell⟨v_{0}⟩ | κ_{0}⟨get, set⟩

in ⟨get_{1}, set_{1}⟩ := mkcell⟨0⟩ ; … set_{1}⟨3⟩ ; … x := get_{1}⟨⟩ ; …

M ⟨v_{0}, κ_{0}⟩ ▷  c⟨v_{0}⟩  κ_{0}⟨..⟩

\begin{matrix}s_{1}⟨u, κ⟩ | c_{1}⟨v⟩ & ▷ c_{1}⟨u⟩ | κ⟨⟩ \\ g_{1}⟨κ⟩ | c_{1}⟨v⟩ & ▷ c_{1}⟨v⟩ | κ⟨v⟩ \end{matrix}  x⟨3⟩

def mkcell⟨v_{0}, κ_{0}⟩ ▷

def set⟨u, κ⟩ | cell⟨v⟩ ▷ cell⟨u⟩ | κ⟨⟩

& get⟨κ⟩ | cell⟨v⟩ ▷ cell⟨v⟩ | κ⟨v⟩

in cell⟨v_{0}⟩ | κ_{0}⟨get, set⟩

in ⟨get_{1}, set_{1}⟩ := mkcell⟨0⟩ ; … set_{1}⟨3⟩ ; … x := get_{1}⟨⟩ ; …

M ⟨v_{0}, κ_{0}⟩ ▷  c⟨v_{0}⟩  κ_{0}⟨..⟩

\begin{matrix}s_{1}⟨u, κ⟩ | c_{1}⟨v⟩ & ▷ c_{1}⟨u⟩ | κ⟨⟩ \\ g_{1}⟨κ⟩ | c_{1}⟨v⟩ & ▷ c_{1}⟨v⟩ | κ⟨v⟩ \end{matrix}

Official formal definition

P =^{def} x⟨\overrightarrow{a}⟩ | def D in P | P | P | 0

D =^{def} J ▷ P | D & D | T

J =^{def} x⟨\overrightarrow{v}⟩ | J | J

def mkcell⟨v_{0}, κ_{0}⟩ ▷

def set⟨u, κ⟩ | cell⟨v⟩ ▷ cell⟨u⟩ | κ⟨⟩

& get⟨κ⟩ | cell⟨v⟩ ▷ cell⟨v⟩ | κ⟨v⟩
in cell⟨v_{0}⟩ | κ_{0}⟨get, set⟩

in … mkcell⟨0, a⟩ … set_{1}⟨3, b⟩ … x := get_{1}⟨⟩ …

Reflexive chemical abstract machines

P =^{def} x⟨\overrightarrow{a}⟩ | def D in P | P | P | 0

D =^{def} J ▷ P | D & D | T

J =^{def} x⟨\overrightarrow{v}⟩ | J | J

multiset of Reac ⊢ multiset of Proc

\begin{matrix}\overrightarrow{x⟨\overrightarrow{v}⟩} ▷ S ⊢ \overrightarrow{x⟨\overrightarrow{a}⟩} & → & \overrightarrow{x⟨\overrightarrow{v}⟩} ▷ S ⊢ S\overrightarrow{[\overrightarrow{v} := \overrightarrow{a}]} \\ ⊢ def D in S & ⇋ & D_{ν} ⊢ S_{ν} \end{matrix}

structural rules on | and &

Distributed RCHAM: multiset of located RCHAM

Type Theory

Theory: formalize mathematics with ▶ typed λ-calculus ▶ Inductive types

▷ related proof and computation principles ▶ Proof theoretic constructs

▷ proof = program Practice ▶ safe proof assistants +++ Coq, LEGO, Agda ▶ tree-like structures ++ ▶ quotients, multisets –

Example

0 : nat S : nat → nat plus : nat → nat → nat

P : nat → Prop P 0 ∀n : nat, P n → P (S n)

nat ind

∀n : nat, P n

nat^{0}  nat S nat  nat nat plus nat
nat^{0} nat^{0} S nat

plus

nat

nat^{0} nat^{0}

plus

nat

S

nat

nat

¡

plus

Concerns

Names and scoping rules (does not depend on TT) ▶ (De Bruijn)^{n+p} ▶ active names Multisets ▶ lists + take ▶ space Mutual inductives ▶ replaced with polymorphic constructs +

extensions by morphism

Structural rules → multisets

P =^{def} x⟨\overrightarrow{a}⟩ | def D in P | P | P | 0

D =^{def} J ▷ P | D & D | T

J =^{def} x⟨\overrightarrow{v}⟩ | J | J

Proc =^{def} x⟨\overrightarrow{a}⟩ | def Def in Sol
Sol =^{def} multiset of Proc
Def =^{def} multiset of Reac
Reac =^{def} multiset of x⟨\overrightarrow{v}⟩ ▷ Sol

Multisets = lists + ternary relations

Thd

∀l : list A, take A x x :: l l

∀l_{1} l_{2} : list A, ∀y : A, take A x l_{1} l_{2} Ttl take A x y :: l_{1} y :: l_{2}

take^{⋆}
take^{+}

Structural rules → lists

P =^{def} x⟨\overrightarrow{a}⟩ | def D in P | P | P | 0

D =^{def} J ▷ P | D & D | T

J =^{def} x⟨\overrightarrow{v}⟩ | J | J

Proc =^{def} x⟨\overrightarrow{a}⟩ | def Def in Sol
Sol =^{def} list Proc
Def =^{def} list Reac
Reac =^{def} list x⟨\overrightarrow{v}⟩ ▷ Sol

Folding mutual inductives

Proc =^{def} x⟨\overrightarrow{a}⟩ | def Def in Sol
Sol =^{def} list Proc
Def =^{def} list Reac
Reac =^{def} list x⟨\overrightarrow{v}⟩ ▷ Sol

The first definition becomes

Proc =^{def} x⟨\overrightarrow{a}⟩
| def (list (list x⟨\overrightarrow{v}⟩ ▷ list Proc) in list Proc

The others are no longer recursive Then use polymorphic combinators

Folding mutual inductives

Fixpoint proc valid at depth (nc np: nat) (p: process)

{struct p}: Prop := match p with | PMessage m ⇒ message valid at depth nc np m | PDef ar lr lp ⇒

fold lreact (proc valid at depth (S nc) (S np)) lr ∧ fold and (proc valid at depth (S nc) np) lp

end.

Definition sol valid at depth (nc np: nat) (lp: solution): Prop := fold and (proc valid at depth nc np) lp.

Definition lreact valid at depth (nc np: nat) (lr: list react): Prop := fold lreact (proc valid at depth nc np) lr.

Names of active channels

Have to be distinguished from names of nested channels

▶ channels used as actual parameters of active messages must

be active Representing deterministic behaviors by non deterministic choices is bad

▶ loss of information ▶ technically: inversions (much) more complicate ⇒

▶ related reactions are grouped together within an automaton

(as in the implementation) ▶ automata are given a unique name ▶ active channel name = ⟨ automaton name, rank ⟩

What is the name of an automaton?

named automata ⊢ list Proc name→automaton ⊢ list Def , list SMsg

automaton : list RMsg × list AReac × arity
RMsg : rank × actual parameters
SMsg : name × rank × actual parameters

It’s just a (logical) location! location→automaton ⊢ list Def , list SMsg

distribution = mapping logical location → physical location

Scopes

Spatial RCHAM

location→automaton ⊢ list Def , list SMsg

Proc =^{def} x⟨\overrightarrow{a}⟩ | def list list … in list Proc
Sol =^{def} list Proc
Reac =^{def} list x⟨\overrightarrow{v}⟩ ▷ Sol
Def =^{def} list Reac

\begin{matrix}\overrightarrow{x⟨\overrightarrow{a}⟩}, \overrightarrow{x⟨\overrightarrow{v}⟩} ▷ S ⊢ & ⟶ & \overrightarrow{x⟨\overrightarrow{v}⟩} ▷ S ⊢ S\overrightarrow{[\overrightarrow{v} := \overrightarrow{a}]} \\ ⊢ def D in S & ⟶ & ∅, D_{ν} ⊢ DS_{ν}, MS_{ν} \\ l ⊢ ⟨p, r, a⟩ & ⟶ & l p.⟨r, a⟩ ⊢ \end{matrix}

Achievements & provocative conclusion

Formal definition completely checked in Coq

(< 1000 lines)

De Bruijn indices correctly handled:

▶ sent messages make sense ▶ two separate kinds of names: active and nested

A better definition of join-calculus:

▶ explicit localities: distribution for free ▶ no structural rules, no reversible rules, no congruences ▶ explicit message migration ▶ conjecture : reversibility of str-def actually does not scale up

to DRCHAM in the original model