Binary communication in the existing π-calculus

DefinitionBinary configuration as a parallel composition#✓fully proved

Embed a binary configuration without changing either process.

def represent (r : Proc × Proc) : Proc := .par r.1 r.2

Uses 1 · Used by 4

Statement usesProcesses of the π-calculus

Used byInjectivity of the binary configuration embedding · Session communication steps are π-calculus reductions · Session communication paths are π-calculus reduction paths · Binary session typing embeds into polarized endpoint typing

TheoremInjectivity of the binary configuration embedding#✓fully proved

The representation does not identify distinct configurations.

theorem represent_injective : Function.Injective represent

Uses 3

Statement usesProcesses of the π-calculus · Binary configuration as a parallel composition

Proof usesChannel name in the π-calculus

InductiveCommunication step of a binary configuration#✓fully proved

Opposite head guards synchronize, in either endpoint orientation.

inductive CommStep : Proc × Proc → Proc × Proc → Prop where
  | send (a : Nat) (b : Name) (p q : Proc) :
      CommStep (.out (.const a) b p, .inp (.const a) q) (p, subst q b)
  | recv (a : Nat) (b : Name) (p q : Proc) :
      CommStep (.inp (.const a) p, .out (.const a) b q) (subst p b, q)

Uses 3 · Used by 5

Statement usesChannel name in the π-calculus · Processes of the π-calculus · Substitution for the innermost bound variable of a process

Used byCommunication preserves binary session typing · Session communication steps are π-calculus reductions · Finite completion of isolated finite binary sessions · Progress for dual single-channel session threads · Session communication paths are π-calculus reduction paths

TheoremSession communication steps are π-calculus reductions#✓fully proved

Every session communication is a reduction in the unchanged π semantics.

theorem represent_step {r t : Proc × Proc} (h : CommStep r t) :
    PiCalculus.Step (represent r) (represent t)

Uses 8 · Used by 1

Statement usesProcesses of the π-calculus · Reduction relation of the π-calculus · Communication step of a binary configuration · Binary configuration as a parallel composition

Proof usesStructural congruence of π-calculus processes · Channel name in the π-calculus · Guarded-choice resolution in the π-calculus · Substitution for the innermost bound variable of a process

Used bySession communication paths are π-calculus reduction paths

DefinitionDual session typing of a binary configuration#✓fully proved

Locally linear threads owning opposite roles on every channel. Dual compatibility permits cyclic waits; it does not assert progress.

def BinaryTyped (Γ : Context) (r : Proc × Proc) : Prop :=
  HasType 0 Γ r.1 ∧ HasType 0 (dualContext Γ) r.2

Uses 4 · Used by 5

Statement usesProcesses of the π-calculus · Per-channel session context of a thread · Linear session typing of sequential threads · Pointwise dual of a session context

Used byCommunication preserves binary session typing · Completed sole protocol means both threads are nil · Finite completion of isolated finite binary sessions · Progress for dual single-channel session threads · Binary session typing embeds into polarized endpoint typing

TheoremCommunication preserves binary session typing#✓fully proved

Communication consumes dual heads and preserves linear residual typing; payload substitution never changes the session context.

theorem CommStep.preservation {Γ : Context} {r t : Proc × Proc}
    (h : CommStep r t) (hr : BinaryTyped Γ r) :
    ∃ a s, (Γ a = .send s ∨ Γ a = .recv s) ∧
      BinaryTyped (advance Γ a s) t

Uses 14

Statement usesProcesses of the π-calculus · Dual session typing of a binary configuration · Communication step of a binary configuration · Per-channel session context of a thread · Finite binary session types · Advancing one endpoint of a session context

Proof usesChannel name in the π-calculus · Name scoped at a binder depth · Substitution for the innermost bound variable of a process · Linear session typing of sequential threads · Receiving a closed name preserves session typing · Dual of a session type · Pointwise dual of a session context · Dualizing a context commutes with advancing an endpoint

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.