Linear endpoint typing for the π-calculus

TheoremBinary session typing embeds into polarized endpoint typing#✓fully proved

Dual original threads embed as disjoint opposite roles on the same physical constants, with exactly their original finite protocol obligations.

theorem binary_hasType {Γ : Cslib.SessionTypes.Context} {r : Proc × Proc}
    (hr : Cslib.SessionTypes.BinaryTyped Γ r) (rank : Nat → Nat) :
    ∃ bound, HasType 0
      (Context.ofFinite Γ bound .positive rank ∪
        Context.ofFinite (Cslib.SessionTypes.dualContext Γ) bound .negative rank)
      (Cslib.SessionTypes.represent r)

abbrev Context := Nat → SessionType

CSLibExt/Languages/SessionTypes/Basic.lean:92

inductive Proc where
  | nil : Proc
  | out (a b : Name) (p : Proc) : Proc
  | inp (a : Name) (p : Proc) : Proc
  | par (p q : Proc) : Proc
  | nu (p : Proc) : Proc
  | repl (p : Proc) : Proc
  | sum (p q : Proc) : Proc
  deriving DecidableEq, Repr

CSLibExt/Languages/PiCalculus/Basic.lean:52

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

CSLibExt/Languages/SessionTypes/Communication.lean:65

inductive HasType : Nat → Context → Proc → Prop where
  | nil {n : Nat} {Δ : Context} :
      Δ.Completed → (∀ e ∈ Δ, e.name.ClosedAt n) → HasType n Δ .nil
  | outName {n : Nat} {Δ : Context} {e : Key} {c : Capability}
      {b : Name} {s : Protocol} {p : Proc} :
      Δ.lookup e = some c → c.protocol.unfold = .sendName s →
      e.name.ClosedAt n → b.ClosedAt n →
      HasType n (Δ.insert e ⟨c.rank, s⟩) p →
      HasType n Δ (.out e.name b p)
  | inpName {n : Nat} {Δ : Context} {e : Key} {c : Capability}
      {s : Protocol} {p : Proc} :
      Δ.lookup e = some c → c.protocol.unfold = .recvName s →
  ⋯

CSLibExt/Languages/SessionTypes/Endpoint/Typing.lean:31

def Context.ofFinite (Γ : Cslib.SessionTypes.Context) (bound : Nat)
    (r : Role) (rank : Nat → Nat) : Context :=
  Finmap.keysLookupEquiv.symm ⟨
    ((Finset.range bound).image (fun i => (⟨.const i, r⟩ : Key)),
      fun e => match e.name with
      | .const i => if e.role = r ∧ i < bound then
          some ⟨rank i, Protocol.ofFinite (Γ i)⟩ else none
      | .var _ => none), by
    rintro ⟨a, s⟩
    cases a with
    | const i =>
      simp only [Option.isSome_ite, Finset.mem_image, Finset.mem_range,
  ⋯

CSLibExt/Languages/SessionTypes/Endpoint/FiniteContext.lean:27

def dualContext (Γ : Context) : Context := fun c => (Γ c).dual

CSLibExt/Languages/SessionTypes/Basic.lean:99

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

CSLibExt/Languages/SessionTypes/Communication.lean:37

Uses 18

Statement usesChannel name in the π-calculus · Processes of the π-calculus · Dual session typing of a binary configuration · Per-channel session context of a thread · Endpoint capability with a dependency rank · Finite endpoint ownership map · Polarized ownership map of a finite channel context · Linear endpoint typing of π-calculus processes · Polarized endpoint key · Endpoint role on a π name · Pointwise dual of a session context · Binary configuration as a parallel composition

Proof usesOwnership maps for opposite roles are disjoint · Finite passive-name typing embeds into endpoint typing · Linear session typing of sequential threads · Session typing derivations have finite support · Finite binary session types · Dual of a session type

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.