Scope preservation for π-calculus names and processes

DefinitionName scoped at a binder depth#✓fully proved

A name refers only to the depth surrounding binders or to a free constant. At depth zero, no variable is permitted.

def Name.ClosedAt (depth : ℕ) : Name → Prop
  | .const _ => True
  | .var i => i < depth

Uses 1 · Used by 210

Statement usesChannel name in the π-calculus

Used byLocally closed processes at a binder depth · Lifting preserves name scoping · Lifting preserves process scoping · Lifting fixes an in-scope name · Lifting fixes a locally closed process · Name substitution preserves scoping · Instantiating the innermost binder preserves process scoping · Substitution at any cutoff preserves process scoping · Communication preserves binary session typing · Session-typed threads are well scoped · 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 · 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 · Structural congruence preserves ranked typing · Erasing a key whose name is absent preserves ranked typing · Minimum active role is the subject of a frontier leaf · Forgetting priorities recovers endpoint typing · Ranked head communication exposes peers and residual typing · Ranked input exposes its subject's guard condition · Inversion of ranked input typing · Adding a role unused by the partner preserves ranked typing · Binder lifting preserves ranked typing · Nil typing lifts to ranked typing · Restriction inversion for ranked typing · Swapping two restrictions preserves ranked typing · Ranked output exposes its subject's guard condition · Inversion of ranked output typing · Parallel inversion for ranked typing · Removing a parallel nil preserves ranked typing · Adding a parallel nil preserves ranked typing · Endpoint delegation at the head preserves ranked typing · Passive head communication preserves ranked typing · Priority-ranked endpoint typing judgement · Collision-free renaming preserves ranked typing · Endpoint substitution preserves ranked typing · Disjoint split supplies freshness for endpoint substitution · Passive substitution preserves ranked typing · Weakening ranked typing by a completed capability · Weakening ranked typing by a disjoint completed context · Endpoint-typed processes are scoped at the ambient depth · Endpoint-typed processes lie in the finite linear fragment · Linear endpoint typing of π-calculus processes · Inversion of endpoint typing for input · Adding a completed capability at nil preserves typing · Inversion of endpoint typing for nil · Nil is typed by a single done capability · Nil is typed by a single capability with completed head · Inversion of endpoint typing for output · Output subjects of endpoint-typed processes are owned · Inversion of endpoint typing for parallel composition · Ownership-map equivalence preserves key scoping · Finite passive-name typing embeds into endpoint typing · The state after both trigger invocations is typed · Nil is runtime-typed with empty ownership · The pending state is typed at the two-role interface · Every phase of the repeated session can step · Each next phase is typed by subject reduction · Every phase is typed at the two-role interface · Every phase is typed by preservation from the pending state · The receiver daemon is typed with empty ownership · The receiver reentry request is runtime-typed · The receiver worker is runtime-typed · Repeated-session traces with typing, availability and progress · Repeated-session traces with preserved typing and availability · The sender daemon is typed with empty ownership · The sender reentry request is runtime-typed · The sender worker is runtime-typed · The state after the sender invocation is typed · Arbitrarily long typed repeated-session traces · Conversion-typed processes are well scoped · Conversion-enabled endpoint typing judgement · Base endpoint typing embeds into conversion typing · Output typing at a code equivalent to one send then end · Output inversion for conversion typing · Owned capabilities with absent names are completed · Erasing a role with an absent name preserves typing · Conversion-typed processes have no sum or replication · Lifting past a binder preserves conversion typing · Typed nil admits a completed scoped capability · Nil inversion for conversion typing · Restriction inversion for conversion typing · Parallel inversion for conversion typing · Removing a parallel nil preserves conversion typing · Collision-free renaming preserves conversion typing · Retyping along ownership-map equivalence · Endpoint substitution preserves conversion typing · Endpoint substitution with freshness from a disjoint split · Passive name substitution preserves conversion typing · Swapping adjacent binders preserves conversion typing · Weakening conversion typing by a completed capability · Weakening conversion typing by a disjoint completed context · Endpoint delegation preserves conversion typing · Head communication preserves conversion typing · Input inversion for conversion typing · Adding a role unused by the partner preserves conversion typing · Adding a parallel nil preserves conversion typing · Passive head communication preserves conversion typing · Restoring the bound pair to the restricted component · Structural congruence preserves conversion typing · Erasing a key whose name is absent preserves conversion ranked typing · Minimum active role is the subject of a conversion frontier leaf · Forgetting priorities yields conversion typing · Conversion-ranked input subjects are active · Nil typing lifts to conversion ranked typing · Restriction inversion for conversion ranked typing · Ranked typing embeds into conversion ranked typing · Conversion-ranked output subjects are active · Parallel inversion for conversion ranked typing · Priority-ranked conversion typing judgement · Weakening conversion ranked typing by a completed capability · Head preservation for a conversion-ranked opposite pair · Inversion of conversion-ranked input typing · Adding a role unused by the partner preserves conversion ranked typing · Binder lifting preserves conversion ranked typing · Endpoint head communication preserves conversion ranked typing · Passive head communication preserves conversion ranked typing · Collision-free renaming preserves conversion ranked typing · Equivalent contexts preserve conversion ranked typing · Endpoint substitution preserves conversion ranked typing · Split-derived freshness for conversion endpoint substitution · Passive substitution preserves conversion ranked typing · Binder swap preserves conversion ranked typing · Weakening conversion ranked typing by a disjoint completed context · Structural congruence preserves conversion ranked typing · Swapping two restrictions preserves conversion ranked typing · Removing a parallel nil preserves conversion ranked typing · Adding a parallel nil preserves conversion ranked typing · Inversion of runtime typing for input on a shared name · Runtime-typed processes are scoped at the ambient depth · Environment extension preserves runtime typing under separation · Runtime typing with guarded shared replication · Output on a declared shared name is a service invocation · Inversion of runtime typing for the nil process · Inversion of runtime typing for restriction · Finite ranked typing embeds into runtime typing under separation · Output subjects are owned endpoints or declared shared names · Inversion of runtime typing for parallel composition · Typed replication has a body with empty ownership · Replicated runtime processes have completed ownership · Runtime typing separates owned names from shared services · Typing rule for a replicated input on a shared name · Owned names absent from a runtime process are completed · Whole owned context of a runtime typing is scoped at ambient depth · Erasing a key whose name is absent preserves runtime typing · Each owned key of a runtime typing is scoped at ambient depth · Removing a restriction around nil preserves runtime typing · Adding a restriction around nil preserves runtime typing · Inversion of runtime typing for replication · Runtime typing transfers to an equivalent linear context · Inversion of runtime typing for a replicated shared input · Typed service templates own only completed entries · Typed service templates retype at empty ownership · Typed service templates retype at any well-formed completed context · Weakening runtime typing by one fresh completed entry · Weakening runtime typing by a disjoint completed context · Structural congruence preserves runtime typing · Runtime typing absorbs a role absent from its parallel partner · Binder lifting preserves runtime typing · Runtime typing under renamings that fix and avoid shared names · Runtime typing under substitution of a transmitted endpoint · Endpoint substitution with side conditions derived from a split · Runtime typing under passive name substitution · Binder swapping preserves runtime typing · Request-free completed runtime frontiers are service templates · Endpoint head communication preserves runtime typing · Minimum active key is the subject of a runtime frontier leaf · Runtime head communication advances or keeps the interface · Runtime inputs are active linear or have completed ownership · Inversion of runtime input on a nonshared subject · Request-free runtime outputs have an active linear subject · Passive head communication preserves runtime typing · Shared invocation and input worker preserve the combined interface · Runtime-typed processes are congruent to a guarded normal form · Same-name linear guards at a compatible interface communicate · Choice selection is the identity on runtime-typed processes · Lifting preserves and reflects name scoping · Weakening by an unused completed endpoint · Structural congruence preserves process scoping · Lifting preserves and reflects process scoping · Swapping binders in scope preserves name scoping · Swapping binders in scope preserves process scoping · Binder lifting preserves endpoint typing · Capture-safe renaming preserves process scope · Removing a parallel nil preserves endpoint typing · Collision-free renaming preserves endpoint typing · Extending a scoped name map under a binder keeps it scoped · Weakening by a disjoint completed context · Owned capability with an absent name is completed · Reduction steps preserve process scoping · Endpoint-delegating communication preserves typing · Endpoint typing drops a role whose name does not occur · Head communication preserves endpoint typing · Passive-payload communication preserves endpoint typing · Endpoint typing under substitution of a transmitted endpoint · Linear subject substitution with freshness from disjoint ownership · Endpoint typing under passive name substitution · Head communication preserves typing and records the matched output · Binder swapping preserves endpoint typing · Semantic advancement preserves scoping of owned keys · Endpoint typing absorbs a role absent from its parallel partner · Inversion of endpoint typing for restriction · Endpoint typing restores both bound roles to the restricted side · Structural congruence preserves endpoint typing · Adding a parallel nil preserves endpoint typing

DefinitionLocally closed processes at a binder depth#✓fully proved

Every variable refers to an enclosing input/restriction binder. ClosedAt 0 permits free constants, but no dangling de Bruijn variables.

def Proc.ClosedAt (depth : ℕ) : Proc → Prop
  | .nil => True
  | .out a b p =>
      a.ClosedAt depth ∧ b.ClosedAt depth ∧ Proc.ClosedAt depth p
  | .inp a p => a.ClosedAt depth ∧ Proc.ClosedAt (depth + 1) p
  | .par p q => Proc.ClosedAt depth p ∧ Proc.ClosedAt depth q
  | .nu p => Proc.ClosedAt (depth + 1) p
  | .repl p => Proc.ClosedAt depth p
  | .sum p q => Proc.ClosedAt depth p ∧ Proc.ClosedAt depth q

Uses 3 · Used by 19

Statement usesChannel name in the π-calculus · Name scoped at a binder depth · Processes of the π-calculus

Used byLifting preserves process scoping · Lifting fixes a locally closed process · Instantiating the innermost binder preserves process scoping · Substitution at any cutoff preserves process scoping · Structural laws are barbed sound in capture-avoiding contexts · Capture-avoiding and lexical filling agree on locally closed holes · Session-typed threads are well scoped · Ranked head communication exposes peers and residual typing · Endpoint-typed processes are scoped at the ambient depth · Conversion-typed processes are well scoped · Runtime-typed processes are scoped at the ambient depth · Structural congruence preserves process scoping · Lifting preserves and reflects process scoping · Choice selection preserves process scoping · Swapping binders in scope preserves process scoping · Capture-safe renaming preserves process scope · Reduction steps preserve process scoping · Head communication preserves endpoint typing · Head communication preserves typing and records the matched output

TheoremLifting fixes an in-scope name#✓fully proved

Lifting above the ambient binder depth fixes an in-scope name.

theorem liftName_eq_of_closedAt {a : Name} {k : ℕ}
    (h : a.ClosedAt k) : liftName k a = a

Uses 3 · Used by 1

Statement usesChannel name in the π-calculus · Name scoped at a binder depth · Lifting free de Bruijn indices of a π-calculus name

Used byLifting fixes a locally closed process

TheoremLifting fixes a locally closed process#✓fully proved

Lifting above the surrounding binders fixes a locally closed process. At depth zero, insertion under a fresh binder cannot capture its names.

theorem liftProc_eq_of_closedAt {p : Proc} {k : ℕ}
    (h : Proc.ClosedAt k p) : liftProc k p = p

Uses 7 · Used by 1

Statement usesProcesses of the π-calculus · Locally closed processes at a binder depth · Lifting free de Bruijn indices of a π-calculus process

Proof usesChannel name in the π-calculus · Name scoped at a binder depth · Lifting free de Bruijn indices of a π-calculus name · Lifting fixes an in-scope name

Used byCapture-avoiding and lexical filling agree on locally closed holes

TheoremLifting preserves name scoping#✓fully proved

Inserting a binder at any cutoff preserves name scoping in the larger environment.

theorem Name.ClosedAt.lift {n k : ℕ} {b : Name} (h : b.ClosedAt n) :
    (liftName k b).ClosedAt (n + 1)

Uses 3 · Used by 10

Statement usesChannel name in the π-calculus · Name scoped at a binder depth · Lifting free de Bruijn indices of a π-calculus name

Used byLifting preserves process scoping · Substitution at any cutoff preserves process scoping · Payload substitution at any cutoff preserves session typing · Binder lifting preserves ranked typing · The receiver worker is runtime-typed · Lifting past a binder preserves conversion typing · Binder lifting preserves conversion ranked typing · Binder lifting preserves runtime typing · Binder lifting preserves endpoint typing · Extending a scoped name map under a binder keeps it scoped

TheoremName substitution preserves scoping#✓fully proved

Removing the binder at k ≤ n preserves name scoping when its replacement is scoped in the remaining environment.

theorem Name.ClosedAt.subst {n k : ℕ} {b x : Name}
    (hb : b.ClosedAt n) (hx : x.ClosedAt (n + 1)) (hk : k ≤ n) :
    (substName b k x).ClosedAt n

Uses 3 · Used by 12

Statement usesChannel name in the π-calculus · Name scoped at a binder depth · Substitution of a name into a π-calculus name

Used bySubstitution at any cutoff preserves process scoping · Payload substitution at any cutoff preserves session typing · Endpoint substitution preserves ranked typing · Passive substitution preserves ranked typing · Endpoint substitution preserves conversion typing · Passive name substitution preserves conversion typing · Endpoint substitution preserves conversion ranked typing · Passive substitution preserves conversion ranked typing · Runtime typing under substitution of a transmitted endpoint · Runtime typing under passive name substitution · Endpoint typing under substitution of a transmitted endpoint · Endpoint typing under passive name substitution

TheoremLifting preserves process scoping#✓fully proved

Shifting a process past a new binder preserves scoping. Inner input and restriction binders increase the cutoff as in Basic.liftProc.

theorem Proc.ClosedAt.lift {p : Proc} {n k : ℕ}
    (h : p.ClosedAt n) : (liftProc k p).ClosedAt (n + 1)

Uses 7

Statement usesProcesses of the π-calculus · Locally closed processes at a binder depth · Lifting free de Bruijn indices of a π-calculus process

Proof usesChannel name in the π-calculus · Name scoped at a binder depth · Lifting preserves name scoping · Lifting free de Bruijn indices of a π-calculus name

TheoremSubstitution at any cutoff preserves process scoping#✓fully proved

Capture-avoiding substitution removes one ambient binder while preserving every name's scope, including under input and restriction.

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

Uses 9 · Used by 1

Statement usesChannel name in the π-calculus · Name scoped at a binder depth · Processes of the π-calculus · Locally closed processes at a binder depth · Substitution of a name into a π-calculus process at a cutoff

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

Used byInstantiating the innermost binder preserves process scoping

TheoremInstantiating the innermost binder preserves process scoping#✓fully proved

Instantiating the innermost binder preserves process scoping.

theorem Proc.ClosedAt.subst {p : Proc} {n : ℕ} {b : Name}
    (h : p.ClosedAt (n + 1)) (hb : b.ClosedAt n) :
    (PiCalculus.subst p b).ClosedAt n

Uses 6 · Used by 1

Statement usesChannel name in the π-calculus · Name scoped at a binder depth · Processes of the π-calculus · Locally closed processes at a binder depth · Substitution for the innermost bound variable of a process

Proof usesSubstitution at any cutoff preserves process scoping

Used byReduction steps preserve process scoping

9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.