General goal

Design a language ▶ for concurrent and distributed programming ▶ that is both expressive and safe

(i.e. it should allows to reason about programs, including types, program analyses, proofs)

Specific goals in this work

A concurrent, object-oriented calculus with:

▶ object internal concurrency

— not just sequential objects running concurrently!

▶ incremental assembling of object definitions

— including the refinement of both ▷ behavior traditional in object-orientation ▷ synchronization expected in a concurrent

Definition of behaviors in the π-calculus

setting u ?(x) P

Reception on u

rec u ?(x) Q

Replicated reception on u

u !(v)  Emission on u u !(w)

dyn!( u )

⋆  u ?(x) S

dyn?( z ) z ?(x) S Too loose!

▶ Behaviors attached to a name are not syntactically known; they are reconfigurable, dynamically.

▶ This makes reasoning and distributed computing difficult.

u ?(x) P
rec u ?(x) Q
u !(v)  u !(w)

dyn!( u )

⋆  u ?(x) S

dyn?( z ) z ?(x) S Too loose!

▶ Behaviors attached to a name are not syntactically known; they are reconfigurable, dynamically.

▶ This makes reasoning and distributed computing difficult.

u ?(x) P
rec u ?(x) Q
u !(v)  u !(w)

dyn!( u )

⋆  u ?(x) S

dyn?( z ) z ?(x) S Too loose!

▶ Behaviors attached to a name are not syntactically known; they are reconfigurable, dynamically.

▶ This makes reasoning and distributed computing difficult.

u ?(x) P
rec u ?(x) Q
u !(v)  u !(w)

dyn!( u )

⋆  u ?(x) S

dyn?( z ) z ?(x) S Too loose!

▶ Behaviors attached to a name are not syntactically known; they are reconfigurable, dynamically.

▶ This makes reasoning and distributed computing difficult.

u ?(x) P
rec u ?(x) Q
u !(v)  u !(w)

dyn!( u )

⋆  u ?(x) S

dyn?( z ) z ?(x) S Too loose!

▶ Behaviors attached to a name are not syntactically known; they are reconfigurable, dynamically.

▶ This makes reasoning and distributed computing difficult.

u ?(x) P
rec u ?(x) Q
u !(v)  u !(w)

dyn!( u )

⋆  u ?(x) S

dyn?( z ) z ?(x) S Too loose!

▶ Behaviors attached to a name are not syntactically known; they are reconfigurable, dynamically.

▶ This makes reasoning and distributed computing difficult.

u ?(x) P
rec u ?(x) Q
u !(v)  u !(w)

dyn!( u )

⋆  u ?(x) S

dyn?( z ) z ?(x) S Too loose!

▶ Behaviors attached to a name are not syntactically known; they are reconfigurable, dynamically.

▶ This makes reasoning and distributed computing difficult.

Definitions of behavior in the join-calculus

\begin{matrix}u (x) ▷ & P \\ u (x) & w (y) ▷ & Q \end{matrix}

Defines synchronizing names u and w and their behaviors altogether

u !(v)

Asynchronous emission on u

w !(v)
…  u !(k)
⋆

dyn( z ) ▷ z !(k)

▶ Name scoping is more constrained than in π-calculus

▶ Easier for reasoning and distributed computation

\begin{matrix}u (x) ▷ & P \\ u (x) & w (y) ▷ & Q \end{matrix}  \begin{aligned}u !(v) \\ & w !(v) \end{aligned}
…  u !(k)
⋆

dyn( z ) ▷ z !(k)

▶ Name scoping is more constrained than in π-calculus

▶ Easier for reasoning and distributed computation

\begin{matrix}u (x) ▷ & P \\ u (x) & w (y) ▷ & Q \end{matrix}  \begin{aligned}u !(v) \\ & w !(v) \end{aligned}
…  u !(k)
⋆

dyn( z ) ▷ z !(k)

▶ Name scoping is more constrained than in π-calculus

▶ Easier for reasoning and distributed computation

\begin{matrix}u (x) ▷ & P \\ u (x) & w (y) ▷ & Q \end{matrix}  \begin{aligned}u !(v) \\ & w !(v) \end{aligned}
…  u !(k)
⋆

dyn( z ) ▷ z !(k)

▶ Name scoping is more constrained than in π-calculus

▶ Easier for reasoning and distributed computation

\begin{matrix}u (x) ▷ & P \\ u (x) & w (y) ▷ & Q \end{matrix}  \begin{aligned}u !(v) \\ & w !(v) \end{aligned}
…  u !(k)
⋆

dyn( z ) ▷ z !(k)

▶ Name scoping is more constrained than in π-calculus

▶ Easier for reasoning and distributed computation

\begin{matrix}u (x) ▷ & P \\ u (x) & w (y) ▷ & Q \end{matrix}  \begin{aligned}u !(v) \\ & w !(v) \end{aligned}
…  u !(k)
⋆

dyn( z ) ▷ z !(k)

▶ Name scoping is more constrained than in π-calculus

▶ Easier for reasoning and distributed computation

\begin{matrix}u (x) ▷ & P \\ u (x) & w (y) ▷ & Q \end{matrix}  \begin{aligned}u !(v) \\ & w !(v) \end{aligned}
…  u !(k)
⋆

dyn( z ) ▷ z !(k)

▶ Name scoping is more constrained than in π-calculus ▷ Behavior of a name is statically defined and

lexically scoped. ▷ Synchronizing names are jointly defined.

▶ Easier for reasoning and distributed computation

\begin{matrix}u (x) ▷ & P \\ u (x) & w (y) ▷ & Q \end{matrix}  \begin{aligned}u !(v) \\ & w !(v) \end{aligned}
…  u !(k)
⋆

dyn( z ) ▷ z !(k)

▶ Name scoping is more constrained than in π-calculus

▶ Easier for reasoning and distributed computation

\begin{matrix}u (x) ▷ & P \\ u (x) & w (y) ▷ & Q \end{matrix}  \begin{aligned}u !(v) \\ & w !(v) \end{aligned}
…  u !(k)
⋆

dyn( z ) ▷ z !(k)

▶ Name scoping is more constrained than in π-calculus

▶ Easier for reasoning and distributed computation