Finite sessions with unrestricted name data

InductiveFinite binary session types#✓fully proved

Finite binary protocols carrying unrestricted, passive names.

inductive SessionType where
  | end : SessionType
  | send (next : SessionType) : SessionType
  | recv (next : SessionType) : SessionType
  deriving DecidableEq, Repr

Used by 31

Used byCommunication preserves binary session typing · Advancing one endpoint of a session context · Session-typed threads are well scoped · Per-channel session context of a thread · Dual of a session type · Dualizing a context commutes with advancing an endpoint · Session type duality is an involution · Session typing derivations have finite support · Linear session typing of sequential threads · Length of a session type · Dual session types have equal length · Payload substitution at any cutoff preserves session typing · The only active channel is the designated one · Advancing the sole channel keeps the single-channel condition · Completed sole protocol means both threads are nil · Dual context keeps the single active channel · Typed thread with completed obligations is nil · Finite completion of isolated finite binary sessions · Progress for dual single-channel session threads · Receive obligation on the sole channel forces an input guard · Send obligation on the sole channel forces an output guard · Single active channel condition for a session context · Binary session typing embeds into polarized endpoint typing · Completed finite contexts give completed ownership maps · Finite ownership map commutes with channel advancement · Embedding of finite passive-name protocols · Finite protocol embedding commutes with duality · Injectivity of the finite protocol embedding · Partial recovery of a finite passive-name protocol · Recovery is a left inverse of the finite embedding · Finite passive-name typing embeds into endpoint typing

DefinitionDual of a session type#✓fully proved

Exchange the endpoint's send and receive obligations.

def SessionType.dual : SessionType → SessionType
  | .end => .end
  | .send s => .recv s.dual
  | .recv s => .send s.dual

Uses 1 · Used by 11

Statement usesFinite binary session types

Used byCommunication preserves binary session typing · Pointwise dual of a session context · Dualizing a context commutes with advancing an endpoint · Session type duality is an involution · Dual session types have equal length · Completed sole protocol means both threads are nil · Dual context keeps the single active channel · Finite completion of isolated finite binary sessions · Progress for dual single-channel session threads · Binary session typing embeds into polarized endpoint typing · Finite protocol embedding commutes with duality

TheoremSession type duality is an involution#✓fully proved

Duality is an involution, including at completion.

@[simp] theorem SessionType.dual_dual (s : SessionType) :
    s.dual.dual = s

Uses 2

Statement usesFinite binary session types · Dual of a session type

DefinitionLength of a session type#✓fully proved

Number of communication actions remaining in a finite protocol.

def SessionType.length : SessionType → Nat
  | .end => 0
  | .send s => s.length + 1
  | .recv s => s.length + 1

Uses 1 · Used by 1

Statement usesFinite binary session types

Used byDual session types have equal length

TheoremDual session types have equal length#✓fully proved

Opposite endpoint roles have the same number of actions.

@[simp] theorem SessionType.length_dual (s : SessionType) :
    s.dual.length = s.length

Uses 3

Statement usesFinite binary session types · Dual of a session type · Length of a session type

AbbreviationPer-channel session context of a thread#✓fully proved

One linear endpoint obligation per physical channel in a thread.

abbrev Context := Nat → SessionType

Uses 1 · Used by 29

Statement usesFinite binary session types

Used byDual session typing of a binary configuration · Communication preserves binary session typing · Advancing one endpoint of a session context · Session-typed threads are well scoped · Pointwise dual of a session context · Dualizing a context commutes with advancing an endpoint · Session typing derivations have finite support · Linear session typing of sequential threads · Receiving a closed name preserves session typing · Payload substitution at any cutoff preserves session typing · The only active channel is the designated one · Advancing the sole channel keeps the single-channel condition · Completed sole protocol means both threads are nil · Dual context keeps the single active channel · Typed thread with completed obligations is nil · Finite completion of isolated finite binary sessions · Progress for dual single-channel session threads · Receive obligation on the sole channel forces an input guard · Send obligation on the sole channel forces an output guard · Single active channel condition for a session context · Binary session typing embeds into polarized endpoint typing · Completed finite contexts give completed ownership maps · Ownership maps for opposite roles are disjoint · Lookup in the finite-context ownership map · Keys of the finite-context ownership map · Polarized ownership map of a finite channel context · Finite ownership map commutes with channel advancement · Binder lift fixes the finite ownership map · Finite passive-name typing embeds into endpoint typing

DefinitionAdvancing one endpoint of a session context#✓fully proved

Advance just the communicating endpoint; other obligations are unchanged.

def advance (Γ : Context) (a : Nat) (s : SessionType) : Context :=
  fun c => if c = a then s else Γ c

Uses 2 · Used by 14

Statement usesPer-channel session context of a thread · Finite binary session types

Used byCommunication preserves binary session typing · Session-typed threads are well scoped · Dualizing a context commutes with advancing an endpoint · Session typing derivations have finite support · Linear session typing of sequential threads · Payload substitution at any cutoff preserves session typing · Advancing the sole channel keeps the single-channel condition · Typed thread with completed obligations is nil · Finite completion of isolated finite binary sessions · Progress for dual single-channel session threads · Receive obligation on the sole channel forces an input guard · Send obligation on the sole channel forces an output guard · Finite ownership map commutes with channel advancement · Finite passive-name typing embeds into endpoint typing

DefinitionPointwise dual of a session context#✓fully proved

The opposite endpoint roles, pointwise.

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

Uses 2 · Used by 8

Statement usesPer-channel session context of a thread · Dual of a session type

Used byDual session typing of a binary configuration · Communication preserves binary session typing · Dualizing a context commutes with advancing an endpoint · Completed sole protocol means both threads are nil · Dual context keeps the single active channel · Finite completion of isolated finite binary sessions · Progress for dual single-channel session threads · Binary session typing embeds into polarized endpoint typing

TheoremDualizing a context commutes with advancing an endpoint#✓fully proved

Advancing dual endpoints preserves pointwise compatibility.

theorem dualContext_advance (Γ : Context) (a : Nat) (s : SessionType) :
    dualContext (advance Γ a s) = advance (dualContext Γ) a s.dual

Uses 5 · Used by 2

Statement usesPer-channel session context of a thread · Finite binary session types · Dual of a session type · Advancing one endpoint of a session context · Pointwise dual of a session context

Used byCommunication preserves binary session typing · Finite completion of isolated finite binary sessions

InductiveLinear session typing of sequential threads#✓fully proved

Linear typing of finite sequential threads in the existing π syntax. nil consumes only completed obligations. Input-bound names are unrestricted payloads, never session subjects; there is no parallel duplication rule.

inductive HasType : Nat → Context → Proc → Prop where
  | nil {n : Nat} {Γ : Context} : (∀ c, Γ c = .end) → HasType n Γ .nil
  | out {n a : Nat} {Γ : Context} {b : Name} {s : SessionType} {p : Proc} :
      Γ a = .send s → b.ClosedAt n → HasType n (advance Γ a s) p →
      HasType n Γ (.out (.const a) b p)
  | inp {n a : Nat} {Γ : Context} {s : SessionType} {p : Proc} :
      Γ a = .recv s → HasType (n + 1) (advance Γ a s) p →
      HasType n Γ (.inp (.const a) p)

Uses 6 · Used by 14

Statement usesChannel name in the π-calculus · Name scoped at a binder depth · Processes of the π-calculus · Per-channel session context of a thread · Finite binary session types · Advancing one endpoint of a session context

Used byDual session typing of a binary configuration · Communication preserves binary session typing · Session-typed threads are well scoped · Session typing derivations have finite support · Receiving a closed name preserves session typing · Payload substitution at any cutoff preserves session typing · Completed sole protocol means both threads are nil · Typed thread with completed obligations is nil · Finite completion of isolated finite binary sessions · Progress for dual single-channel session threads · Receive obligation on the sole channel forces an input guard · Send obligation on the sole channel forces an output guard · Binary session typing embeds into polarized endpoint typing · Finite passive-name typing embeds into endpoint typing

TheoremPayload substitution at any cutoff preserves session typing#✓fully proved

Capture-avoiding payload substitution preserves every linear obligation, including through nested input binders and at nonzero cutoffs.

theorem HasType.substProc {n k : Nat} {Γ : Context} {p : Proc} {b : Name}
    (h : HasType (n + 1) Γ p) (hb : b.ClosedAt n) (hk : k ≤ n) :
    HasType n Γ (PiCalculus.substProc b k p)

Uses 12 · Used by 1

Statement usesChannel name in the π-calculus · Name scoped at a binder depth · Processes of the π-calculus · Substitution of a name into a π-calculus process at a cutoff · Per-channel session context of a thread · Linear session typing of sequential threads

Proof usesLifting preserves name scoping · Name substitution preserves scoping · Lifting free de Bruijn indices of a π-calculus name · Substitution of a name into a π-calculus name · Finite binary session types · Advancing one endpoint of a session context

Used byReceiving a closed name preserves session typing

TheoremReceiving a closed name preserves session typing#✓fully proved

Receiving a closed name preserves the residual thread's typing.

theorem HasType.subst {Γ : Context} {p : Proc} {b : Name}
    (h : HasType 1 Γ p) (hb : b.ClosedAt 0) :
    HasType 0 Γ (PiCalculus.subst p b)

Uses 7 · Used by 2

Statement usesChannel name in the π-calculus · Name scoped at a binder depth · Processes of the π-calculus · Substitution for the innermost bound variable of a process · Per-channel session context of a thread · Linear session typing of sequential threads

Proof usesPayload substitution at any cutoff preserves session typing

Used byCommunication preserves binary session typing · Finite completion of isolated finite binary sessions

TheoremSession typing derivations have finite support#✓fully proved

A derivation has only finitely many active channel obligations: above some bound every channel is completed. Contexts are total functions.

theorem HasType.finite_support {n : Nat} {Γ : Context} {p : Proc}
    (h : HasType n Γ p) : ∃ bound, ∀ c, bound ≤ c → Γ c = .end

Uses 7 · Used by 1

Statement usesProcesses of the π-calculus · Per-channel session context of a thread · Linear session typing of sequential threads · Finite binary session types

Proof usesChannel name in the π-calculus · Name scoped at a binder depth · Advancing one endpoint of a session context

Used byBinary session typing embeds into polarized endpoint typing

TheoremSession-typed threads are well scoped#✓fully proved

Every typed thread satisfies the shared π name/process scoping predicate. Free session constants remain permitted; this is not ν-closedness.

theorem HasType.closedAt {n : Nat} {Γ : Context} {p : Proc}
    (h : HasType n Γ p) : p.ClosedAt n

Uses 8

Statement usesProcesses of the π-calculus · Locally closed processes at a binder depth · Per-channel session context of a thread · Linear session typing of sequential threads

Proof usesChannel name in the π-calculus · Name scoped at a binder depth · Finite binary session types · Advancing one endpoint of a session context

14 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.