The π-calculus: syntax, substitution, structural congruence, reduction

InductiveChannel name in the π-calculus#✓fully proved

A channel name: a free channel const n, or the i-th enclosing binder var i.

inductive Name where
  | const (n : ℕ) : Name
  | var (i : ℕ) : Name
  deriving DecidableEq, Repr

Used by 609

Used byName scoped at a binder depth · Locally 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 · Barbs of an input prefix · The inactive process has no barbs · Barbs of a restricted output prefix · Barbs of an output prefix · Unguarded output in a process · Every reduction source has an unguarded output · Structural congruence preserves unguarded outputs · Free-channel input is not barbed bisimilar to nil · Free-channel guard offered without reduction · Composition of process contexts · One-hole lexical process contexts · Lexical filling of a process context · Structural congruence is closed under contexts · Capture-avoiding filling of a process context · Capture-avoiding and lexical filling agree on locally closed holes · Filling a composed context is iterated filling · Structural congruence of π-calculus processes · Lifting free de Bruijn indices of a π-calculus name · Lifting free de Bruijn indices of a π-calculus process · Processes of the π-calculus · Reduction relation of the π-calculus · Substitution for the innermost bound variable of a process · Substitution of a name into a π-calculus name · Substitution leaves constant channels and the empty process unchanged · Substitution of a name into a π-calculus process at a cutoff · Swapping adjacent de Bruijn indices in a name · Swapping adjacent binders throughout a process · Communication step of a binary configuration · Communication preserves binary session typing · Injectivity of the binary configuration embedding · Session communication steps are π-calculus reductions · 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 · Existence of a least-rank active binding · Active delegated payloads rank after the guard · Binding a fresh dual pair preserves balance · Completed ranked frontiers are congruent to nil · Structural congruence preserves ranked typing · Erasing a role preserves the guard condition · Erasing a key whose name is absent preserves ranked typing · Minimum active role is the subject of a frontier leaf · Every finite linear π term has a frontier normal form · Parallel guard frontier · Guard priority condition on active endpoints · An active same-rank peer violates the guard condition · A guard owning only its own endpoint satisfies the condition · Forgetting priorities recovers endpoint typing · Ranked head communication yields a dual advance · Ranked head communication exposes peers and residual typing · Ranked input subjects are active · Ranked input exposes its subject's guard condition · Inversion of ranked input typing · Active roles on other names rank after an input subject · Adding a completed role preserves the guard condition · Adding a role unused by the partner preserves ranked typing · Lifting preserves guard frontiers · Binder lifting preserves ranked typing · A minimum active role owned by a guard is its subject key · Minimum guard leaf cannot own its dual peer · Nil typing lifts to ranked typing · Restriction inversion for ranked typing · Swapping two restrictions preserves ranked typing · Ranked output subjects are active · Ranked output exposes its subject's guard condition · Inversion of ranked output typing · Parallel reassociation preserves ranked typing · Reverse parallel reassociation preserves ranked typing · Parallel commutation preserves ranked typing · Parallel inversion for ranked typing · Removing a parallel nil preserves ranked typing · Adding a parallel nil preserves ranked typing · Progress for balanced ranked guard frontiers · Endpoint delegation at the head preserves ranked typing · Passive head communication preserves ranked typing · Priority-ranked endpoint typing judgement · Injective rekeying preserves the guard condition · Collision-free renaming preserves ranked typing · Restoring the bound pair preserves ranked typing · Same-name ranked guards are opposite and communicate · Forward scope extrusion preserves ranked typing · Reverse scope extrusion preserves ranked typing · Subject reduction for ranked typing at compatible interfaces · Ranked subject reduction at the empty interface · Endpoint substitution preserves ranked typing · Disjoint split supplies freshness for endpoint substitution · Passive substitution preserves ranked typing · Ranked typing descends from a lifted process · Weakening ranked typing by a completed capability · Weakening ranked typing by a disjoint completed context · Balanced endpoint ownership · A fresh restriction pair is balanced · The empty interface is balanced · Compatibility of a partial endpoint interface · Balanced interfaces are compatible · Disjoint owned keys on one name have opposite roles · Rekeying preserves balance · Compatibility passes to the left part of a union · Compatibility passes to the right part of a disjoint split · Binary session typing embeds into polarized endpoint typing · Binding a fresh dual pair under restriction · Restriction binding over the empty map · Entries of a restriction-bound ownership map · Restriction binding preserves absence of an outer key · Both roles of the new name are fresh for a lifted map · Negative role lookup after restriction binding · Positive role lookup after restriction binding · Lookups in a lifted ownership map · Injectivity of rekeying survives erasing a key · Injectivity of rekeying survives updating an owned key · Injectivity of rekeying under a restriction binding · Rekeying under a binder is injective on fresh and lifted keys · Injectivity of rekeying passes under a binder · Injectivity of rekeying after receiving a fresh role · Linear input installs the received role on the bound name · Received role's opposite is absent at the bound name · Rekeying commutes with binding a private pair · Rekeying under a binder is the lift of the outer rekeying · Binder extension fixes the fresh binder's endpoint keys · Binder extension commutes with lifting on endpoint keys · Completed ownership map · The empty ownership map is completed · Erasing a key preserves completion · Inserting a completed capability preserves completion · Lookups in a rekeyed ownership map · Rekeying preserves completion · Uniqueness of capability lookups · Finite linear π fragment without choice or replication · Structural congruence preserves the finite linear fragment · Lifting preserves and reflects the finite linear fragment · Reduction preserves the finite linear fragment · Substitution preserves and reflects the finite linear fragment · Restriction swap preserves and reflects the finite linear fragment · Restriction binding commutes with erasing an owned outer key · Restriction binding commutes with inserting an outer key · Restriction binding of a disjoint union · Binding a fresh pair keeps disjointness from a lifted context · Erase-and-insert transfer preserves disjointness · Inserting a key absent from the other side preserves disjointness · Updating an owned key preserves a disjoint split · Capability transfer with carrier updates preserves disjointness · Erasing the bound pair leaves the lifted context · Erasing a different key commutes with insertion · Erasure after inserting the same key · Erasing an absent key changes nothing · Erasure distributes over union · Updating an owned key keeps absent keys absent · Owned keys are absent from the other side of a disjoint split · Insertion after erasing the same key · Reinserting an owned capability changes nothing · Inserting a left-absent key into a union updates the right part · Context lifting commutes with erasing an owned key · Context lifting commutes with insertion · Context lifting preserves a disjoint union · Collision-free rekeying commutes with erasing an owned key · Collision-free rekeying commutes with insertion · Collision-free rekeying commutes with a disjoint union · Reinstalling the bound pair after erasing its slots · Moving a capability across a union preserves the union · Combined context after delegation and two carrier updates · Updating owned keys on both sides of a disjoint union · 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 · 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 · Binding equivalent fresh pairs preserves ownership-map equivalence · Ownership-map equivalence preserves semantic compatibility · Ownership-map equivalence preserves completion · Pointwise equivalence of ownership maps · Erasure preserves ownership-map equivalence · Equivalent insertions preserve ownership-map equivalence · Lifting preserves ownership-map equivalence · Lookups transfer along ownership-map equivalence · Lookups in a key projection · Equivalent ownership maps have the same keys · Keys of a projection are the intersection of domains · Ownership-map equivalence from two-way lookup correspondence · Projection of an ownership map onto another map's keys · Key projection agrees with the target inside the source domain · Key projection is absent outside the source domain · Equivalence of a union restricts to its left part · Reflexivity of ownership-map equivalence · Ownership-map equivalence preserves key scoping · Equivalent capabilities give equivalent singleton maps · Equivalence of a disjoint union splits into equivalent parts · Symmetry of ownership-map equivalence · Transitivity of ownership-map equivalence · Union preserves ownership-map equivalence · Distinct keys on one name are opposite · Extensionality for endpoint keys · Polarized endpoint key · Renaming the physical name of an endpoint key · Injective renamings act injectively on endpoint keys · Peer endpoint key · An endpoint key differs from its peer · Key reversal is an involution · Binder lift fixes the finite ownership map · Finite passive-name typing embeds into endpoint typing · Unguarded shared input communicates with a matching output · State after both trigger invocations · The state after both trigger invocations is typed · Every phase of the restricted repeated session can step · Endpoint distinct from both service triggers · A fresh endpoint singleton is separated from the triggers · Erasing a singleton's only key leaves the empty map · All declared services are available in the pending state · Lifting preserves trigger freshness of an endpoint · Nil is runtime-typed with empty ownership · Idle processes have no unguarded output · Offered service communicates with a matching shared output · Persistent service offers survive one reduction step · Pending state with two role transfers · The pending state is typed at the two-role interface · Phases of the repeated-session execution · Services stay available at every phase · Every phase of the repeated session can step · Both services are offered at every phase · Every phase is reachable from the pending state · Each phase steps to the next · 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 · Replicated receiver daemon · The receiver daemon is typed with empty ownership · Sender-invoked state steps by invoking the receiver trigger · Receiver-role transfer to its trigger · The receiver reentry request is runtime-typed · Data substitution yields the receiver's return request · Substitution instantiates the receiver worker's endpoint · Receiver worker process · The receiver worker is runtime-typed · Semantic advances of the recurring interface are the identity · The recurring interface is balanced · Two-role linear interface of the recurring session · Steps preserve typing at the recurring interface · Every round count has a trace returning to the pending state · Repeated-session traces with typing, availability and progress · Repeated-session traces with preserved typing and availability · Replicated sender daemon · The sender daemon is typed with empty ownership · Pending state steps by invoking the sender trigger · Sender-role transfer to its trigger · The sender reentry request is runtime-typed · Substitution instantiates the sender worker's endpoint · Sender worker process · The sender worker is runtime-typed · State after the sender trigger invocation · The state after the sender invocation is typed · Invoking a replicated service is a reduction step · Session action steps back to the pending state · Every round has a session action on the same endpoint · Arbitrarily long typed repeated-session traces · Conversion-typed processes are well scoped · Semantic peer compatibility of an ownership map · Syntactic compatibility implies semantic compatibility · 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 · Communicating subjects have semantically dual capabilities · 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 update leaves the transmitted payload slot unchanged · Head communication preserves conversion typing · Head update leaves other lookups unchanged · Input inversion for conversion typing · Adding a role unused by the partner preserves conversion typing · Removing a restriction around nil preserves conversion typing · Adding a restriction around nil preserves conversion typing · Parallel reassociation preserves conversion typing · Reverse parallel reassociation preserves conversion typing · Parallel commutation preserves conversion typing · Adding a parallel nil preserves conversion typing · Passive head communication preserves conversion typing · Restoring the bound pair to the restricted component · Forward scope extrusion preserves conversion typing · Reverse scope extrusion preserves conversion typing · Lowering a lifted process preserves conversion typing · Completed conversion-ranked frontiers are congruent to nil · 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 · Minimum guard leaf cannot own an equivalent dual peer · 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 · Subject reduction at a compatible conversion interface · Subject reduction at the empty interface · Weakening conversion ranked typing by a completed capability · Conversion head communication yields a semantic advance · 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 · Progress for semantically balanced conversion frontiers · Endpoint head communication preserves conversion ranked typing · Passive head communication preserves conversion ranked typing · Collision-free renaming preserves conversion ranked typing · Equivalent contexts preserve the guard condition · Equivalent contexts preserve conversion ranked typing · Same-name conversion guards are opposite and communicate · Forward scope extrusion preserves 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 · Conversion ranked typing descends from a lifted process · Weakening conversion ranked typing by a disjoint completed context · Structural congruence preserves conversion ranked typing · Swapping two restrictions preserves conversion ranked typing · Parallel reassociation preserves conversion ranked typing · Reverse parallel reassociation preserves conversion ranked typing · Parallel commutation preserves conversion ranked typing · Removing a parallel nil preserves conversion ranked typing · Adding a parallel nil preserves conversion ranked typing · Restoring the bound pair preserves conversion ranked typing · Reverse scope extrusion preserves conversion ranked typing · Conversion ranked subject reduction at compatible interfaces · Conversion ranked subject reduction at the empty interface · Structural congruence preserves unguarded shared inputs · Unguarded shared input on a given name · Service templates are invariant under structural congruence · Priority of a shared invocation over active owned keys · Invocation priority for a singleton of rank above the priority · Service templates are invariant under lifting · Offered services have an unguarded shared input · Structural congruence preserves persistent service offers · Persistent service offer on a given name · Separation of owned linear names from shared names · Empty ownership is separated from shared names · Singleton context with a nonshared name is separated · Structural shared-service template · Service templates are invariant under binder swapping · Erasing an owned key preserves nonaliasing · Erasing an owned key preserves separation · Name map fixing every declared shared constant · Inserting a nonshared key preserves separation · Updating an already-owned key preserves nonaliasing · Nonaliasing of owned-name images with shared constants · Every name map is nonaliasing on empty ownership · Separation gives nonaliasing for binder lifting · Separation gives nonaliasing for binder swapping · Rekeying preserves shared invocation priority · Rekeying the empty context gives the empty context · Rekeying a singleton moves its key and keeps its capability · Service templates are preserved by renamings fixing shared names · Rekeying along a nonaliasing name map yields separation · Binder extension preserves fixing of shared constants · Nonaliasing survives binding a private session pair · Binder extension preserves nonaliasing of lifted contexts · Nonaliasing survives adding a received parameter under a binder · Nonaliasing restricts to the left part of a union · Nonaliasing restricts to the right part of a union · Inversion of runtime typing for input on a shared name · Binding a private pair preserves separation · Runtime-typed processes are scoped at the ambient depth · Service templates survive environment extension · Environment extension preserves runtime typing under separation · Runtime typing with guarded shared replication · Output on a declared shared name is a service invocation · Binder lifting preserves separation · 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 · Separation restricts to the left part of a union · Separation restricts to the right part of a disjoint union · Owned names absent from a runtime process are completed · Whole owned context of a runtime typing is scoped at ambient depth · Erasing an owned key preserves invocation priority · Erasing a key whose name is absent preserves runtime typing · Inserting a completed entry preserves invocation priority · 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 · Equivalent retyping preserves separation from shared names · Equivalent retyping preserves invocation priority · Runtime typing transfers to an equivalent linear context · Inversion of runtime typing for a replicated shared input · Typed replicated shared inputs are offered services · 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 · Guarded frontier of guards and idle service templates · Runtime typing absorbs a role absent from its parallel partner · Binder lifting preserves runtime typing · Request-freeness is invariant under lifting · Passive substitution creates no owned shared-name alias · Nonshared endpoint substitution keeps owned names nonshared · Runtime typing under renamings that fix and avoid shared names · Process with no exposed output on a declared shared name · Runtime typing restores both bound roles to the restricted side · Runtime typing is preserved by forward scope extrusion · Runtime typing is preserved by reverse scope extrusion · 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-freeness is invariant under binder swapping · Runtime typing reflects through binder lifting · Semantic advance preserves shared-linear separation · Request-free completed runtime frontiers are service templates · Request-freeness is invariant under structural congruence · Endpoint head communication preserves runtime typing · Minimum active key is the subject of a runtime frontier leaf · Non-request-free frontier exposes a shared output up to congruence · Runtime head communication advances or keeps the interface · Runtime inputs are active linear or have completed ownership · Lifting preserves guarded frontiers · Inversion of runtime input on a nonshared subject · Request-free runtime outputs have an active linear subject · Runtime minimum guard leaf cannot own an equivalent dual peer · Passive head communication preserves runtime typing · Service templates are request-free · Exposed shared requests step when declared services are available · Shared invocation and input worker preserve the combined interface · Runtime-typed processes are congruent to a guarded normal form · Balanced runtime frontiers are idle or step given availability · Same-name linear guards at a compatible interface communicate · Choice selection is the identity on runtime-typed processes · Subject reduction for runtime typing at compatible interfaces · Subject reduction for runtime typing at the empty interface · Lifting preserves and reflects name scoping · Unguarded input in a process · Structural congruence preserves unguarded inputs · Injectivity of name lifting · Commutation of name lifts at ordered cutoffs · Commuting a name lift past a lift at cutoff zero · A lifted name is never the innermost binder · A lifted key is never a freshly bound key · Commutation of process lifts at ordered cutoffs · Absence of a physical name from a process · The inserted name is absent from a lifted process · An output payload name is not absent · Every π step source has an unguarded input · Substitution cancels name lifting · Substitution cancels process lifting · Injectivity of name swapping · Name swap is an involution · Process swap is an involution · 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 of processes · Capture-safe renaming preserves process scope · Process renaming by a lift is process lifting · Process renaming by a substitution is process substitution · Process renaming by a swap is the restriction swap · Removing a parallel nil preserves endpoint typing · Collision-free renaming preserves endpoint typing · Extension of a name map under a binder · Extending a lift under a binder raises its cutoff · Extended name map commutes with lifting outer names · Extending a scoped name map under a binder keeps it scoped · Extending a substitution under a binder raises its cutoff · Extending a swap under a binder shifts both indices · Weakening by a disjoint completed context · Owned capability with an absent name is completed · Reduction steps preserve process scoping · Communicating subjects in a compatible split have dual capabilities · Communicating subjects in a compatible split have equal ranks · Endpoint-delegating communication preserves typing · Endpoint typing drops a role whose name does not occur · Head communication preserves endpoint typing · Passive substitution is injective on lifted outer keys · Received-endpoint substitution is injective when the role is fresh · Matched output head of a capability · Passive-payload communication preserves endpoint typing · Passive substitution leaves the linear context unchanged · Received-endpoint substitution moves the bound role to the sent key · Endpoint typing under substitution of a transmitted endpoint · Linear subject substitution with freshness from disjoint ownership · Substitution cancels lifting on endpoint keys · Endpoint typing under passive name substitution · Dual advancement preserves balance · Dual advancement preserves compatibility · Advancement of a matched dual subject pair · Dual-continuation update preserves balance · Dual-continuation update preserves compatibility · Dual-continuation update leaves other lookups unchanged · Subject lookup after a dual-continuation update · Dual advancement in the left part of a union · Dual advancement in the right part of a disjoint union · Head communication yields a dual advancement · Head communication preserves typing and records the matched output · Dual advancement preserves the owned keys · A matched output head is a send with the same continuation · Binder swapping preserves endpoint typing · Swapping nested restrictions exchanges their bound pairs · Swapping the two innermost binders fixes a twice-lifted context · Context swapping commutes with insertion · Semantic balance of a linear context · Semantic advancement preserves balance · The empty context is semantically balanced · Raw balance implies semantic balance · Semantic balance implies semantic compatibility · Semantic advancement preserves compatibility · Semantic advancement extends from the left part to the whole union · Semantic advancement extends from the right part to a disjoint union · Typed head communication yields a semantic advancement · Lifting preserves semantic advancement · Semantic advancement preserves the context's domain · Raw dual advancement is a semantic advancement · Semantic advancement preserves capability ranks · Semantic advancement preserves scoping of owned keys · Semantic advancement of a communicating endpoint pair · Binder swapping preserves semantic advancement · Semantic advancement is raw under literal compatibility · Outer insertion commutes with binding a fresh pair · Outer dual advancement lifts through restriction · Lowering preserves disjointness of outer contexts · Erasing both roles of the fresh name leaves outer keys · Lowering is injective on contexts without fresh-name keys · Endpoint typing absorbs a role absent from its parallel partner · Lifting a lowered context recovers it · Lowering then lifting an outer key returns it · Context lifting is injective · Outer lookups pass through a freshly bound pair · Lowering of an outer context past a fresh binder · Inversion of endpoint typing for restriction · Dual advancement under restriction splits into inner and outer cases · Dual advancement under restriction splits, keeping the private step · Endpoint typing restores both bound roles to the restricted side · Endpoint typing is preserved by forward scope extrusion · Endpoint typing is preserved by reverse scope extrusion · Endpoint typing reflects through binder lifting · Updating both bound roles, negative first, rebinds the pair · Updating both bound roles, positive first, rebinds the pair · Binding a dual private pair preserves compatibility · Binding a dual private pair preserves balance · Binding a fresh dual pair preserves dual compatibility · Outer semantic advances lift past a private binding · Structural congruence preserves endpoint typing · Removing a restriction around nil preserves endpoint typing · Adding a restriction around nil preserves endpoint typing · Parallel reassociation preserves endpoint typing · Reverse parallel reassociation preserves endpoint typing · Parallel commutation preserves endpoint typing · Adding a parallel nil preserves endpoint typing · Semantic advance under a private binding is private or outer · Injective rekeying preserves dual compatibility · Equivalent retyping preserves semantic balance · Union of disjoint balanced contexts is balanced · Compatibility restricts to the left part of a union · Compatibility restricts to the right part of a disjoint union · Subject reduction for endpoint typing at compatible interfaces · Subject reduction for endpoint typing at the empty interface

InductiveProcesses of the π-calculus#✓fully proved

Processes of the π-calculus. inp a p binds variable 0 in p; nu p binds variable 0 in p as a fresh channel.

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

Uses 1 · Used by 448

Statement usesChannel name in the π-calculus

Used byLocally closed processes at a binder depth · Lifting preserves process scoping · Lifting fixes a locally closed process · Instantiating the innermost binder preserves process scoping · Substitution at any cutoff preserves process scoping · Immediate free-channel barb · Structural congruence preserves immediate barbs · Barbed bisimilar processes have the same barbs · Barbs of an input prefix · The inactive process has no barbs · Barbs of a restricted output prefix · Barbs of an output prefix · Strong barbed bisimilarity · Structurally congruent processes are barbed bisimilar · Structural congruence is a strong barbed bisimulation · Unguarded output in a process · Every reduction source has an unguarded output · Structural congruence preserves unguarded outputs · Free-channel input is not barbed bisimilar to nil · Decorated-LTS bisimulations are exactly strong barbed bisimulations · May-barb after finitely many reductions · Barbed bisimilarity preserves may-barbs · Processes without unguarded output cannot reduce · Reduction LTS decorated with barb observations · Exposed guards are barbs · Free-channel guard offered without reduction · Barbed bisimilarity transfers finite reduction paths · Barbed bisimilarity matches each reduction by one reduction · Contextual barbed equivalence implies barbed bisimilarity · Composition of process contexts · One-hole lexical process contexts · Contextual strong barbed equivalence · Structural congruence implies contextual barbed equivalence · Lexical filling of a process context · Structural congruence is closed under contexts · Contextual barbed equivalence is closed under contexts · Capture-avoiding filling of a process context · Structural laws are barbed sound in capture-avoiding contexts · Capture-avoiding and lexical filling agree on locally closed holes · Filling a composed context is iterated filling · Structural congruence of π-calculus processes · Lifting free de Bruijn indices of a π-calculus process · Guarded-choice resolution in the π-calculus · Reduction relation of the π-calculus · Substitution for the innermost bound variable of a process · Substitution leaves constant channels and the empty process unchanged · Substitution of a name into a π-calculus process at a cutoff · Swapping adjacent binders throughout a process · Dual session typing of a binary configuration · Communication step of a binary configuration · Communication preserves binary session typing · Binary configuration as a parallel composition · Injectivity of the binary configuration embedding · Session communication steps are π-calculus reductions · 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 · 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 · Session communication paths are π-calculus reduction paths · Send obligation on the sole channel forces an output guard · Completed ranked frontiers are congruent to nil · 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 · Every finite linear π term has a frontier normal form · Frontier normal form of finite networks · Ranked-typed processes have a typed frontier normal form · Parallel guard frontier · Forgetting priorities recovers endpoint typing · Ranked head communication yields a dual advance · Ranked head communication exposes peers and residual typing · Ranked input subjects are active · Ranked input exposes its subject's guard condition · Inversion of ranked input typing · Active roles on other names rank after an input subject · Adding a role unused by the partner preserves ranked typing · Lifting preserves guard frontiers · Lifting preserves frontier normal form · Binder lifting preserves ranked typing · Minimum guard leaf cannot own its dual peer · Nil typing lifts to ranked typing · Restriction inversion for ranked typing · Removing a restriction around nil preserves ranked typing · Restricting nil preserves ranked typing · Swapping two restrictions preserves ranked typing · Reverse restriction swap preserves ranked typing · Ranked output subjects are active · Ranked output exposes its subject's guard condition · Inversion of ranked output typing · Parallel reassociation preserves ranked typing · Reverse parallel reassociation preserves ranked typing · Parallel commutation preserves ranked typing · Parallel inversion for ranked typing · Removing a parallel nil preserves ranked typing · Adding a parallel nil preserves ranked typing · Parallel composition of frontier normal forms normalizes · Progress for balanced ranked guard frontiers · Global progress of ranked processes at balanced interfaces · Closed ranked networks are completed or can step · Endpoint delegation at the head preserves ranked typing · Passive head communication preserves ranked typing · Priority-ranked endpoint typing judgement · Reachable states of closed ranked networks stay typed · Progress at reachable states of closed ranked networks · Collision-free renaming preserves ranked typing · Restoring the bound pair preserves ranked typing · Same-name ranked guards are opposite and communicate · Forward scope extrusion preserves ranked typing · Ranked typing is invariant under scope extrusion · Reverse scope extrusion preserves ranked typing · Subject reduction for ranked typing at compatible interfaces · Ranked subject reduction at balanced interfaces · Ranked subject reduction at the empty interface · Endpoint substitution preserves ranked typing · Disjoint split supplies freshness for endpoint substitution · Passive substitution preserves ranked typing · Ranked typing descends from a lifted process · Weakening ranked typing by a completed capability · Weakening ranked typing by a disjoint completed context · Binary session typing embeds into polarized endpoint typing · Finite linear π fragment without choice or replication · Structural congruence preserves the finite linear fragment · Lifting preserves and reflects the finite linear fragment · Selection is trivial on the choice-free fragment · Reduction preserves the finite linear fragment · Substitution preserves and reflects the finite linear fragment · Restriction swap preserves and reflects the finite linear fragment · 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 · Finite passive-name typing embeds into endpoint typing · Unguarded shared input communicates with a matching output · Availability of all declared services · Availability as offers of all declared signatures · State after both trigger invocations · The state after both trigger invocations is typed · Every phase of the restricted repeated session can step · Structural congruence preserves service availability · Nil is runtime-typed with empty ownership · Idle processes cannot step · Idle processes have no unguarded output · Offered service communicates with a matching shared output · Selection preserves persistent offers · Persistent service offers survive one reduction step · Interchange law for four parallel components · Pending state with two role transfers · The pending state is typed at the two-role interface · Phases of the repeated-session execution · Every phase of the repeated session can step · Both services are offered at every phase · Every phase is reachable from the pending state · Each phase steps to the next · Every phase is typed at the two-role interface · Declared signature offers survive finite reduction · Service availability survives finite reduction · Replicated receiver daemon · Sender-invoked state steps by invoking the receiver trigger · Receiver-role transfer to its trigger · The receiver reentry request is runtime-typed · Data substitution yields the receiver's return request · Substitution instantiates the receiver worker's endpoint · Receiver worker process · The receiver worker is runtime-typed · Steps preserve typing at the recurring interface · Every round count has a trace returning to the pending state · Repeated-session traces with typing, availability and progress · Repeated-session traces with preserved typing and availability · Replicated sender daemon · Pending state steps by invoking the sender trigger · Sender-role transfer to its trigger · The sender reentry request is runtime-typed · Substitution instantiates the sender worker's endpoint · Sender worker process · The sender worker is runtime-typed · State after the sender trigger invocation · The state after the sender invocation is typed · Invoking a replicated service is a reduction step · Session action steps back to the pending state · Every round has a session action on the same endpoint · Declared signature offers survive one reduction step · Service availability survives one reduction step · 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 · Ownership-map equivalence preserves typing in both directions · 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 · Removing a restriction around nil preserves conversion typing · Adding a restriction around nil preserves conversion typing · Swapping nested restrictions preserves conversion typing · Parallel reassociation preserves conversion typing · Reverse parallel reassociation preserves conversion typing · Parallel commutation preserves conversion typing · Adding a parallel nil preserves conversion typing · Passive head communication preserves conversion typing · Restoring the bound pair to the restricted component · Forward scope extrusion preserves conversion typing · Scope extrusion preserves conversion typing in both directions · Reverse scope extrusion preserves conversion typing · Lowering a lifted process preserves conversion typing · Completed conversion-ranked frontiers are congruent to nil · 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 · Minimum guard leaf cannot own an equivalent dual peer · Nil typing lifts to conversion ranked typing · Restriction inversion for conversion ranked typing · Reverse restriction swap preserves conversion 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 · Typing and compatibility persist along finite executions · Empty-interface typing persists along finite executions · Subject reduction at a compatible conversion interface · Subject reduction at a balanced interface · Subject reduction at the empty interface · Weakening conversion ranked typing by a completed capability · Conversion head communication yields a semantic advance · 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 · Progress for semantically balanced conversion frontiers · 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 · Context equivalence transports conversion ranked typing both ways · Same-name conversion guards are opposite and communicate · Forward scope extrusion preserves 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 · Conversion ranked typing descends from a lifted process · Weakening conversion ranked typing by a disjoint completed context · Structural congruence preserves conversion ranked typing · Conversion-ranked processes have a typed frontier normal form · Removing a restriction around nil preserves conversion ranked typing · Restricting nil preserves conversion ranked typing · Swapping two restrictions preserves conversion ranked typing · Reverse restriction swap preserves conversion ranked typing · Parallel reassociation preserves conversion ranked typing · Reverse parallel reassociation preserves conversion ranked typing · Parallel commutation preserves conversion ranked typing · Removing a parallel nil preserves conversion ranked typing · Adding a parallel nil preserves conversion ranked typing · Global progress of conversion-ranked processes at balanced interfaces · Finite runs keep conversion ranked typing at compatible interfaces · Reachable closed conversion-ranked states keep the empty interface · Restoring the bound pair preserves conversion ranked typing · Conversion ranked typing is invariant under scope extrusion · Reverse scope extrusion preserves conversion ranked typing · Conversion ranked subject reduction at compatible interfaces · Conversion ranked subject reduction at balanced interfaces · Conversion ranked subject reduction at the empty interface · Closed conversion-ranked networks are completed or can step · Progress at reachable states of closed conversion-ranked networks · Structural congruence preserves unguarded shared inputs · Unguarded shared input on a given name · Service templates are invariant under structural congruence · Declared service offers are invariant under congruence · Idleness is invariant under structural congruence · Idle process as a structural service template · Service templates are invariant under lifting · Declared persistent service offer · Offered services have an unguarded shared input · Structural congruence preserves persistent service offers · Persistent service offer on a given name · Structural shared-service template · Service templates are invariant under binder swapping · Service templates are preserved by renamings fixing shared names · Inversion of runtime typing for input on a shared name · Runtime-typed processes are scoped at the ambient depth · Service templates survive environment extension · 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 · Runtime typing is invariant under equivalent linear contexts · Inversion of runtime typing for a replicated shared input · Typed replicated shared inputs are offered services · 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 · Guarded frontier of guards and idle service templates · Guarded normal form: restrictions over a guarded frontier · Runtime typing absorbs a role absent from its parallel partner · Binder lifting preserves runtime typing · Request-freeness is invariant under lifting · Runtime typing under renamings that fix and avoid shared names · Process with no exposed output on a declared shared name · Runtime typing restores both bound roles to the restricted side · Runtime typing is preserved by forward scope extrusion · Runtime typing is invariant under scope extrusion · Runtime typing is preserved by reverse scope extrusion · 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-freeness is invariant under binder swapping · Runtime typing reflects through binder lifting · Request-free completed runtime frontiers are service templates · Request-freeness is invariant under structural congruence · Endpoint head communication preserves runtime typing · Minimum active key is the subject of a runtime frontier leaf · Non-request-free frontier exposes a shared output up to congruence · Guarded normal form of a typed process keeps its typing · Runtime head communication advances or keeps the interface · Runtime inputs are active linear or have completed ownership · Lifting preserves guarded frontiers · Lifting preserves guarded normal forms · Inversion of runtime input on a nonshared subject · Request-free runtime outputs have an active linear subject · Runtime minimum guard leaf cannot own an equivalent dual peer · Parallel composition preserves guarded normal forms up to congruence · Passive head communication preserves runtime typing · Service templates are request-free · Exposed shared requests step when declared services are available · Shared invocation and input worker preserve the combined interface · Runtime-typed processes are congruent to a guarded normal form · Balanced runtime frontiers are idle or step given availability · Global runtime progress at balanced interfaces given availability · Closed runtime processes are idle or step given availability · Multi-step subject reduction at compatible interfaces · Multi-step subject reduction at balanced interfaces · Multi-step subject reduction at the empty interface · Qualified progress at every reachable runtime state · Qualified progress at reachable closed runtime states · Same-name linear guards at a compatible interface communicate · Choice selection is the identity on runtime-typed processes · Subject reduction for runtime typing at compatible interfaces · Subject reduction for runtime typing at balanced interfaces · Subject reduction for runtime typing at the empty interface · Unguarded input in a process · Structural congruence preserves unguarded inputs · Selection reflects unguarded inputs · Commutation of process lifts at ordered cutoffs · Absence of a physical name from a process · The inserted name is absent from a lifted process · An output payload name is not absent · Every π step source has an unguarded input · Substitution cancels process lifting · Process swap is an involution · Weakening by an unused completed endpoint · Structural congruence preserves process scoping · Lifting preserves and reflects process scoping · Choice selection preserves process scoping · Swapping binders in scope preserves process scoping · Binder lifting preserves endpoint typing · Capture-safe renaming of processes · Capture-safe renaming preserves process scope · Process renaming by a lift is process lifting · Process renaming by a substitution is process substitution · Process renaming by a swap is the restriction swap · Removing a parallel nil preserves endpoint typing · Collision-free renaming preserves endpoint typing · 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 yields a dual advancement · Head communication preserves typing and records the matched output · Binder swapping preserves endpoint typing · Typed head communication yields a semantic advancement · 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 · Endpoint typing is preserved by forward scope extrusion · Endpoint typing is preserved by reverse scope extrusion · Endpoint typing reflects through binder lifting · Structural congruence preserves endpoint typing · Removing a restriction around nil preserves endpoint typing · Adding a restriction around nil preserves endpoint typing · Swapping nested restrictions preserves endpoint typing · Reverse restriction swap preserves endpoint typing · Parallel reassociation preserves endpoint typing · Reverse parallel reassociation preserves endpoint typing · Parallel commutation preserves endpoint typing · Adding a parallel nil preserves endpoint typing · Endpoint typing is invariant under scope extrusion · Subject reduction for endpoint typing at compatible interfaces · Subject reduction for endpoint typing at balanced interfaces · Subject reduction for endpoint typing at the empty interface

DefinitionLifting free de Bruijn indices of a π-calculus name#✓fully proved

Shift free variables at or above cutoff up by one, e.g. when pushing a process under a binder.

def liftName (cutoff : ℕ) : Name → Name
  | .const n => .const n
  | .var i => if cutoff ≤ i then .var (i + 1) else .var i

Uses 1 · Used by 115

Statement usesChannel name in the π-calculus

Used byLifting preserves name scoping · Lifting preserves process scoping · Lifting fixes an in-scope name · Lifting fixes a locally closed process · Substitution at any cutoff preserves process scoping · Barbs of an input prefix · The inactive process has no barbs · Barbs of a restricted output prefix · Barbs of an output prefix · Structural congruence preserves unguarded outputs · Lifting free de Bruijn indices of a π-calculus process · Substitution of a name into a π-calculus process at a cutoff · Payload substitution at any cutoff preserves session typing · Binding a fresh dual pair preserves balance · Erasing a key whose name is absent preserves ranked typing · Lifting preserves guard frontiers · Binder lifting preserves ranked typing · Weakening ranked typing by a completed capability · Restriction binding preserves absence of an outer key · Both roles of the new name are fresh for a lifted map · Lifting preserves absence of a key · Lifting an ownership map past a binder · Lifting a singleton ownership map · Lookups in a lifted ownership map · Rekeying under a binder is injective on fresh and lifted keys · Injectivity of rekeying passes under a binder · Rekeying under a binder is the lift of the outer rekeying · Binder extension commutes with lifting on endpoint keys · Lifting preserves and reflects the finite linear fragment · Substitution preserves and reflects the finite linear fragment · Restriction binding commutes with erasing an owned outer key · Restriction binding commutes with inserting an outer key · Binding a fresh pair keeps disjointness from a lifted context · Context lifting commutes with erasing an owned key · Context lifting commutes with insertion · Context lifting preserves a disjoint union · Lifting preserves ownership-map equivalence · Binder lift fixes the finite ownership map · Unguarded shared input communicates with a matching output · Every phase of the restricted repeated session can step · Lifting preserves trigger freshness of an endpoint · Every phase of the repeated session can step · Data substitution yields the receiver's return request · Receiver worker process · The receiver worker is runtime-typed · Session action steps back to the pending state · Owned capabilities with absent names are completed · Erasing a role with an absent name preserves typing · Lifting past a binder preserves conversion typing · Weakening conversion typing by a completed capability · Erasing a key whose name is absent preserves conversion ranked typing · Weakening conversion ranked typing by a completed capability · Binder lifting preserves conversion ranked typing · Structural congruence preserves unguarded shared inputs · Service templates are invariant under lifting · Structural congruence preserves persistent service offers · Separation gives nonaliasing for binder lifting · Binder extension preserves fixing of shared constants · Binder extension preserves nonaliasing of lifted contexts · Binder lifting preserves separation · Owned names absent from a runtime process are completed · Erasing a key whose name is absent preserves runtime typing · Each owned key of a runtime typing is scoped at ambient depth · Adding a restriction around nil preserves runtime typing · Typed service templates own only completed entries · Typed service templates retype at any well-formed completed context · Weakening runtime typing by one fresh completed entry · Binder lifting preserves runtime typing · Request-freeness is invariant under lifting · Lifting preserves guarded frontiers · Lifting preserves and reflects name scoping · Structural congruence preserves unguarded inputs · Injectivity of name lifting · Commutation of name lifts at ordered cutoffs · Commuting a name lift past a lift at cutoff zero · A lifted name is never the innermost binder · A lifted key is never a freshly bound key · Commutation of process lifts at ordered cutoffs · Absence of a physical name from a process · The inserted name is absent from a lifted process · Substitution cancels name lifting · Substitution cancels process lifting · Weakening by an unused completed endpoint · Lifting preserves and reflects process scoping · Binder lifting preserves endpoint typing · Process renaming by a lift is process lifting · Process renaming by a substitution is process substitution · Extension of a name map under a binder · Extending a lift under a binder raises its cutoff · Extended name map commutes with lifting outer names · Extending a substitution under a binder raises its cutoff · Owned capability with an absent name is completed · Endpoint typing drops a role whose name does not occur · Passive substitution is injective on lifted outer keys · Received-endpoint substitution is injective when the role is fresh · Passive substitution leaves the linear context unchanged · Received-endpoint substitution moves the bound role to the sent key · Substitution cancels lifting on endpoint keys · Swapping nested restrictions exchanges their bound pairs · Swapping the two innermost binders fixes a twice-lifted context · Lifting preserves semantic advancement · Outer insertion commutes with binding a fresh pair · Outer dual advancement lifts through restriction · Lowering is injective on contexts without fresh-name keys · Lifting a lowered context recovers it · Lowering then lifting an outer key returns it · Context lifting is injective · Outer lookups pass through a freshly bound pair · Dual advancement under restriction splits into inner and outer cases · Dual advancement under restriction splits, keeping the private step · Binding a dual private pair preserves compatibility · Binding a dual private pair preserves balance · Binding a fresh dual pair preserves dual compatibility · Outer semantic advances lift past a private binding · Semantic advance under a private binding is private or outer

DefinitionLifting free de Bruijn indices of a π-calculus process#✓fully proved

Shift free variables of a process, entering binders with an increased cutoff.

def liftProc (cutoff : ℕ) : Proc → Proc
  | .nil => .nil
  | .out a b p => .out (liftName cutoff a) (liftName cutoff b) (liftProc cutoff p)
  | .inp a p => .inp (liftName cutoff a) (liftProc (cutoff + 1) p)
  | .par p q => .par (liftProc cutoff p) (liftProc cutoff q)
  | .nu p => .nu (liftProc (cutoff + 1) p)
  | .repl p => .repl (liftProc cutoff p)
  | .sum p q => .sum (liftProc cutoff p) (liftProc cutoff q)

Uses 3 · Used by 69

Statement usesChannel name in the π-calculus · Processes of the π-calculus · Lifting free de Bruijn indices of a π-calculus name

Used byLifting preserves process scoping · Lifting fixes a locally closed process · Barbs of an input prefix · The inactive process has no barbs · Barbs of a restricted output prefix · Barbs of an output prefix · Structural congruence preserves unguarded outputs · Capture-avoiding filling of a process context · Capture-avoiding and lexical filling agree on locally closed holes · Structural congruence of π-calculus processes · Structural congruence preserves ranked typing · Lifting preserves guard frontiers · Lifting preserves frontier normal form · Binder lifting preserves ranked typing · Parallel composition of frontier normal forms normalizes · Restoring the bound pair preserves ranked typing · Forward scope extrusion preserves ranked typing · Ranked typing is invariant under scope extrusion · Reverse scope extrusion preserves ranked typing · Ranked typing descends from a lifted process · Structural congruence preserves the finite linear fragment · Lifting preserves and reflects the finite linear fragment · Unguarded shared input communicates with a matching output · Lifting past a binder preserves conversion typing · Adding a restriction around nil preserves conversion typing · Restoring the bound pair to the restricted component · Forward scope extrusion preserves conversion typing · Scope extrusion preserves conversion typing in both directions · Reverse scope extrusion preserves conversion typing · Lowering a lifted process preserves conversion typing · Structural congruence preserves conversion typing · Binder lifting preserves conversion ranked typing · Forward scope extrusion preserves conversion ranked typing · Conversion ranked typing descends from a lifted process · Structural congruence preserves conversion ranked typing · Restoring the bound pair preserves conversion ranked typing · Conversion ranked typing is invariant under scope extrusion · Reverse scope extrusion preserves conversion ranked typing · Structural congruence preserves unguarded shared inputs · Service templates are invariant under structural congruence · Service templates are invariant under lifting · Structural congruence preserves persistent service offers · Structural congruence preserves runtime typing · Binder lifting preserves runtime typing · Request-freeness is invariant under lifting · Runtime typing restores both bound roles to the restricted side · Runtime typing is preserved by forward scope extrusion · Runtime typing is invariant under scope extrusion · Runtime typing is preserved by reverse scope extrusion · Runtime typing reflects through binder lifting · Request-freeness is invariant under structural congruence · Lifting preserves guarded frontiers · Lifting preserves guarded normal forms · Parallel composition preserves guarded normal forms up to congruence · Structural congruence preserves unguarded inputs · Commutation of process lifts at ordered cutoffs · The inserted name is absent from a lifted process · Substitution cancels process lifting · Structural congruence preserves process scoping · Lifting preserves and reflects process scoping · Binder lifting preserves endpoint typing · Process renaming by a lift is process lifting · Endpoint typing restores both bound roles to the restricted side · Endpoint typing is preserved by forward scope extrusion · Endpoint typing is preserved by reverse scope extrusion · Endpoint typing reflects through binder lifting · Structural congruence preserves endpoint typing · Adding a restriction around nil preserves endpoint typing · Endpoint typing is invariant under scope extrusion

DefinitionSubstitution of a name into a π-calculus name#✓fully proved

Substitute the name n for the variable at cutoff: variables below the cutoff are bound by inner binders and untouched, the variable at the cutoff is replaced by n, and variables above shift down by one.

def substName (n : Name) : ℕ → Name → Name
  | _, .const m => .const m
  | cutoff, .var i =>
      if i < cutoff then .var i
      else if i = cutoff then n
      else .var (i - 1)

Uses 1 · Used by 40

Statement usesChannel name in the π-calculus

Used byName substitution preserves scoping · Substitution at any cutoff preserves process scoping · Substitution of a name into a π-calculus process at a cutoff · Payload substitution at any cutoff preserves session typing · Binding a fresh dual pair preserves balance · Endpoint substitution preserves ranked typing · Passive substitution preserves ranked typing · Substitution preserves and reflects the finite linear fragment · Data substitution yields the receiver's return request · Endpoint substitution preserves conversion typing · Passive name substitution preserves conversion typing · Endpoint substitution preserves conversion ranked typing · Passive substitution preserves conversion ranked typing · Passive substitution creates no owned shared-name alias · Nonshared endpoint substitution keeps owned names nonshared · Runtime typing under substitution of a transmitted endpoint · Runtime typing under passive name substitution · Injectivity of name lifting · Substitution cancels name lifting · Substitution cancels process lifting · Process renaming by a substitution is process substitution · Extending a substitution under a binder raises its cutoff · Passive substitution is injective on lifted outer keys · Received-endpoint substitution is injective when the role is fresh · Passive substitution leaves the linear context unchanged · Received-endpoint substitution moves the bound role to the sent key · Endpoint typing under substitution of a transmitted endpoint · Substitution cancels lifting on endpoint keys · Endpoint typing under passive name substitution · Lowering preserves disjointness of outer contexts · Lowering is injective on contexts without fresh-name keys · Lifting a lowered context recovers it · Lowering then lifting an outer key returns it · Lowering of an outer context past a fresh binder · Dual advancement under restriction splits into inner and outer cases · Dual advancement under restriction splits, keeping the private step · Binding a dual private pair preserves compatibility · Binding a dual private pair preserves balance · Binding a fresh dual pair preserves dual compatibility · Semantic advance under a private binding is private or outer

DefinitionSubstitution of a name into a π-calculus process at a cutoff#✓fully proved

Substitute the name n for the variable at cutoff in a process. Under a binder, n is lifted by one at cutoff 0 so it keeps referring to the same outer names: every free index of n refers to a binder above the substitution point, so all of them shift. Lifting at the current cutoff would leave indices below the cutoff captured by the new binder.

def substProc (n : Name) : ℕ → Proc → Proc
  | _, .nil => .nil
  | cutoff, .out a b p =>
      .out (substName n cutoff a) (substName n cutoff b) (substProc n cutoff p)
  | cutoff, .inp a p =>
      .inp (substName n cutoff a) (substProc (liftName 0 n) (cutoff + 1) p)
  | cutoff, .par p q => .par (substProc n cutoff p) (substProc n cutoff q)
  | cutoff, .nu p => .nu (substProc (liftName 0 n) (cutoff + 1) p)
  | cutoff, .repl p => .repl (substProc n cutoff p)
  | cutoff, .sum p q => .sum (substProc n cutoff p) (substProc n cutoff q)

Uses 4 · Used by 22

Statement usesChannel name in the π-calculus · Processes of the π-calculus · Lifting free de Bruijn indices of a π-calculus name · Substitution of a name into a π-calculus name

Used bySubstitution at any cutoff preserves process scoping · Substitution for the innermost bound variable of a process · Payload substitution at any cutoff preserves session typing · Endpoint substitution preserves ranked typing · Passive substitution preserves ranked typing · Ranked typing descends from a lifted process · Reduction preserves the finite linear fragment · Substitution preserves and reflects the finite linear fragment · Endpoint substitution preserves conversion typing · Passive name substitution preserves conversion typing · Lowering a lifted process preserves conversion typing · Endpoint substitution preserves conversion ranked typing · Passive substitution preserves conversion ranked typing · Conversion ranked typing descends from a lifted process · Runtime typing under substitution of a transmitted endpoint · Runtime typing under passive name substitution · Runtime typing reflects through binder lifting · Substitution cancels process lifting · Process renaming by a substitution is process substitution · Endpoint typing under substitution of a transmitted endpoint · Endpoint typing under passive name substitution · Endpoint typing reflects through binder lifting

DefinitionSubstitution for the innermost bound variable of a process#✓fully proved

Substitute the name n for the innermost bound variable of p.

def subst (p : Proc) (n : Name) : Proc := substProc n 0 p

Uses 3 · Used by 71

Statement usesChannel name in the π-calculus · Processes of the π-calculus · Substitution of a name into a π-calculus process at a cutoff

Used byInstantiating the innermost binder preserves process scoping · Every reduction source has an unguarded output · Reduction relation of the π-calculus · Substitution leaves constant channels and the empty process unchanged · Communication step of a binary configuration · Communication preserves binary session typing · Session communication steps are π-calculus reductions · Receiving a closed name preserves session typing · Finite completion of isolated finite binary sessions · Progress for dual single-channel session threads · Ranked head communication yields a dual advance · Ranked head communication exposes peers and residual typing · Endpoint delegation at the head preserves ranked typing · Passive head communication preserves ranked typing · Same-name ranked guards are opposite and communicate · Subject reduction for ranked typing at compatible interfaces · Endpoint substitution preserves ranked typing · Disjoint split supplies freshness for endpoint substitution · Passive substitution preserves ranked typing · Ranked typing descends from a lifted process · Reduction preserves the finite linear fragment · Unguarded shared input communicates with a matching output · Persistent service offers survive one reduction step · Data substitution yields the receiver's return request · Substitution instantiates the receiver worker's endpoint · Substitution instantiates the sender worker's endpoint · Invoking a replicated service is a reduction step · Session action steps back to the pending state · Endpoint substitution preserves conversion typing · Endpoint substitution with freshness from a disjoint split · Passive name substitution preserves conversion typing · Endpoint delegation preserves conversion typing · Head communication preserves conversion typing · Removing a restriction around nil preserves conversion typing · Passive head communication preserves conversion typing · Lowering a lifted process preserves conversion typing · Subject reduction at a compatible conversion interface · Conversion head communication yields a semantic advance · Head preservation for a conversion-ranked opposite pair · Endpoint head communication preserves conversion ranked typing · Passive head communication preserves conversion ranked typing · Same-name conversion guards are opposite and communicate · Endpoint substitution preserves conversion ranked typing · Split-derived freshness for conversion endpoint substitution · Passive substitution preserves conversion ranked typing · Conversion ranked typing descends from a lifted process · Conversion ranked subject reduction at compatible interfaces · Runtime typing under substitution of a transmitted endpoint · Endpoint substitution with side conditions derived from a split · Runtime typing under passive name substitution · Runtime typing reflects through binder lifting · Endpoint head communication preserves runtime typing · Runtime head communication advances or keeps the interface · Passive head communication preserves runtime typing · Shared invocation and input worker preserve the combined interface · Same-name linear guards at a compatible interface communicate · Subject reduction for runtime typing at compatible interfaces · Every π step source has an unguarded input · Reduction steps preserve process scoping · Endpoint-delegating communication preserves typing · 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 yields a dual advancement · Head communication preserves typing and records the matched output · Typed head communication yields a semantic advancement · Endpoint typing reflects through binder lifting · Removing a restriction around nil preserves endpoint typing · Subject reduction for endpoint typing at compatible interfaces

DefinitionSwapping adjacent de Bruijn indices in a name#✓fully proved

Swap the two de Bruijn indices cutoff and cutoff + 1 in a name: the two binders at that depth exchange places.

def swapNameAt (cutoff : ℕ) : Name → Name
  | .var i => if i = cutoff then .var (cutoff + 1)
      else if i = cutoff + 1 then .var cutoff else .var i
  | .const n => .const n

Uses 1 · Used by 31

Statement usesChannel name in the π-calculus

Used byBarbs of an input prefix · The inactive process has no barbs · Barbs of a restricted output prefix · Barbs of an output prefix · Structural congruence preserves unguarded outputs · Swapping adjacent binders throughout a process · Swapping two restrictions preserves ranked typing · Restriction swap preserves and reflects the finite linear fragment · Swapping adjacent binders preserves conversion typing · Binder swap preserves conversion ranked typing · Swapping two restrictions preserves conversion ranked typing · Structural congruence preserves unguarded shared inputs · Structural congruence preserves persistent service offers · Service templates are invariant under binder swapping · Separation gives nonaliasing for binder swapping · Binder swapping preserves runtime typing · Request-freeness is invariant under binder swapping · Structural congruence preserves unguarded inputs · Injectivity of name swapping · Name swap is an involution · Process swap is an involution · Swapping binders in scope preserves name scoping · Swapping binders in scope preserves process scoping · Process renaming by a swap is the restriction swap · Extending a swap under a binder shifts both indices · Swapping two ambient binders in an ownership context · Binder swapping preserves endpoint typing · Swapping nested restrictions exchanges their bound pairs · Swapping the two innermost binders fixes a twice-lifted context · Context swapping commutes with insertion · Binder swapping preserves semantic advancement

DefinitionSwapping adjacent binders throughout a process#✓fully proved

Swap the two binders at depth cutoff throughout a process, incrementing the cutoff under binders.

def swapProc (cutoff : ℕ) : Proc → Proc
  | .nil => .nil
  | .out a b p => .out (swapNameAt cutoff a) (swapNameAt cutoff b) (swapProc cutoff p)
  | .inp a p => .inp (swapNameAt cutoff a) (swapProc (cutoff + 1) p)
  | .par p q => .par (swapProc cutoff p) (swapProc cutoff q)
  | .nu p => .nu (swapProc (cutoff + 1) p)
  | .repl p => .repl (swapProc cutoff p)
  | .sum p q => .sum (swapProc cutoff p) (swapProc cutoff q)

Uses 3 · Used by 36

Statement usesChannel name in the π-calculus · Processes of the π-calculus · Swapping adjacent de Bruijn indices in a name

Used byBarbs of an input prefix · The inactive process has no barbs · Barbs of a restricted output prefix · Barbs of an output prefix · Structural congruence preserves unguarded outputs · Structural congruence of π-calculus processes · Structural congruence preserves ranked typing · Swapping two restrictions preserves ranked typing · Reverse restriction swap preserves ranked typing · Structural congruence preserves the finite linear fragment · Restriction swap preserves and reflects the finite linear fragment · Swapping adjacent binders preserves conversion typing · Swapping nested restrictions preserves conversion typing · Structural congruence preserves conversion typing · Reverse restriction swap preserves conversion typing · Binder swap preserves conversion ranked typing · Structural congruence preserves conversion ranked typing · Swapping two restrictions preserves conversion ranked typing · Reverse restriction swap preserves conversion ranked typing · Structural congruence preserves unguarded shared inputs · Service templates are invariant under structural congruence · Structural congruence preserves persistent service offers · Service templates are invariant under binder swapping · Structural congruence preserves runtime typing · Binder swapping preserves runtime typing · Request-freeness is invariant under binder swapping · Request-freeness is invariant under structural congruence · Structural congruence preserves unguarded inputs · Process swap is an involution · Structural congruence preserves process scoping · Swapping binders in scope preserves process scoping · Process renaming by a swap is the restriction swap · Binder swapping preserves endpoint typing · Structural congruence preserves endpoint typing · Swapping nested restrictions preserves endpoint typing · Reverse restriction swap preserves endpoint typing

TheoremSubstitution leaves constant channels and the empty process unchanged#✓fully proved

Substitution leaves a process with no var 0 untouched: a constant channel stays constant, and the empty process stays empty.

theorem subst_nil (n : Name) : subst .nil n = .nil

Uses 3

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

InductiveStructural congruence of π-calculus processes#✓fully proved

Structural congruence: | is commutative and associative with unit nil, ν extrudes over | (lifting the other side, which cannot mention the fresh name), restriction of nil is nil, nested restrictions commute (swapping the two bound indices), and replication unfolds.

Cslib.PiCalculus.Cong · 22 lines

inductive Cong : Proc → Proc → Prop
  | refl (p : Proc) : Cong p p
  | symm {p q : Proc} : Cong p q → Cong q p
  | trans {p q r : Proc} : Cong p q → Cong q r → Cong p r
  | par_comm (p q : Proc) : Cong (.par p q) (.par q p)
  | par_assoc (p q r : Proc) : Cong (.par (.par p q) r) (.par p (.par q r))
  | par_nil (p : Proc) : Cong (.par p .nil) p
  | par_cong {p p' q q' : Proc} : Cong p p' → Cong q q' →
      Cong (.par p q) (.par p' q')
  | nu_cong {p p' : Proc} : Cong p p' → Cong (.nu p) (.nu p')
  | scope (p q : Proc) :
      Cong (.par (.nu p) q) (.nu (.par p (liftProc 0 q)))
  | sum_cong {p p' q q' : Proc} : Cong p p' → Cong q q' →
      Cong (.sum p q) (.sum p' q')
  | out_cong {p p' : Proc} (a b : Name) : Cong p p' →
      Cong (.out a b p) (.out a b p')
  | inp_cong {q q' : Proc} (a : Name) : Cong q q' →
      Cong (.inp a q) (.inp a q')
  | repl_cong {p p' : Proc} : Cong p p' → Cong (.repl p) (.repl p')
  | nu_nil : Cong (.nu .nil) .nil
  | nu_swap (p : Proc) : Cong (.nu (.nu p)) (.nu (.nu (swapProc 0 p)))
  | repl_unfold (p : Proc) : Cong (.repl p) (.par p (.repl p))

Uses 4 · Used by 71

Statement usesChannel name in the π-calculus · Processes of the π-calculus · Lifting free de Bruijn indices of a π-calculus process · Swapping adjacent binders throughout a process

Used byImmediate free-channel barb · Structural congruence preserves immediate barbs · Barbs of an input prefix · The inactive process has no barbs · Barbs of a restricted output prefix · Barbs of an output prefix · Structurally congruent processes are barbed bisimilar · Structural congruence is a strong barbed bisimulation · Every reduction source has an unguarded output · Structural congruence preserves unguarded outputs · Exposed guards are barbs · Structural congruence implies contextual barbed equivalence · Structural congruence is closed under contexts · Structural laws are barbed sound in capture-avoiding contexts · Reduction relation of the π-calculus · Session communication steps are π-calculus reductions · Completed ranked frontiers are congruent to nil · Structural congruence preserves ranked typing · Minimum active role is the subject of a frontier leaf · Every finite linear π term has a frontier normal form · Ranked-typed processes have a typed frontier normal form · Parallel composition of frontier normal forms normalizes · Progress for balanced ranked guard frontiers · Global progress of ranked processes at balanced interfaces · Closed ranked networks are completed or can step · Progress at reachable states of closed ranked networks · Same-name ranked guards are opposite and communicate · Subject reduction for ranked typing at compatible interfaces · Structural congruence preserves the finite linear fragment · Reduction preserves the finite linear fragment · Unguarded shared input communicates with a matching output · Structural congruence preserves service availability · Persistent service offers survive one reduction step · Interchange law for four parallel components · Invoking a replicated service is a reduction step · Session action steps back to the pending state · Completed conversion-ranked frontiers are congruent to nil · Structural congruence preserves conversion typing · Minimum active role is the subject of a conversion frontier leaf · Subject reduction at a compatible conversion interface · Progress for semantically balanced conversion frontiers · Same-name conversion guards are opposite and communicate · Structural congruence preserves conversion ranked typing · Conversion-ranked processes have a typed frontier normal form · Global progress of conversion-ranked processes at balanced interfaces · Conversion ranked subject reduction at compatible interfaces · Closed conversion-ranked networks are completed or can step · Progress at reachable states of closed conversion-ranked networks · Structural congruence preserves unguarded shared inputs · Service templates are invariant under structural congruence · Declared service offers are invariant under congruence · Idleness is invariant under structural congruence · Structural congruence preserves persistent service offers · Structural congruence preserves runtime typing · Request-freeness is invariant under structural congruence · Minimum active key is the subject of a runtime frontier leaf · Non-request-free frontier exposes a shared output up to congruence · Guarded normal form of a typed process keeps its typing · Parallel composition preserves guarded normal forms up to congruence · Exposed shared requests step when declared services are available · Runtime-typed processes are congruent to a guarded normal form · Balanced runtime frontiers are idle or step given availability · Global runtime progress at balanced interfaces given availability · Same-name linear guards at a compatible interface communicate · Subject reduction for runtime typing at compatible interfaces · Structural congruence preserves unguarded inputs · Every π step source has an unguarded input · Structural congruence preserves process scoping · Reduction steps preserve process scoping · Structural congruence preserves endpoint typing · Subject reduction for endpoint typing at compatible interfaces

InductiveGuarded-choice resolution in the π-calculus#✓fully proved

Guarded-choice resolution: discard sum branches to reach a guarded process. Transitivity handles nested sums.

inductive Select : Proc → Proc → Prop
  | refl (p : Proc) : Select p p
  | left (p q : Proc) : Select (.sum p q) p
  | right (p q : Proc) : Select (.sum p q) q
  | trans {p q r : Proc} : Select p q → Select q r → Select p r

Uses 1 · Used by 29

Statement usesProcesses of the π-calculus

Used byBarbs of an input prefix · The inactive process has no barbs · Barbs of a restricted output prefix · Barbs of an output prefix · Every reduction source has an unguarded output · Free-channel input is not barbed bisimilar to nil · Free-channel guard offered without reduction · Reduction relation of the π-calculus · Session communication steps are π-calculus reductions · Same-name ranked guards are opposite and communicate · Subject reduction for ranked typing at compatible interfaces · Selection is trivial on the choice-free fragment · Reduction preserves the finite linear fragment · Unguarded shared input communicates with a matching output · Selection preserves persistent offers · Persistent service offers survive one reduction step · Invoking a replicated service is a reduction step · Session action steps back to the pending state · Subject reduction at a compatible conversion interface · Same-name conversion guards are opposite and communicate · Conversion ranked subject reduction at compatible interfaces · Same-name linear guards at a compatible interface communicate · Choice selection is the identity on runtime-typed processes · Subject reduction for runtime typing at compatible interfaces · Selection reflects unguarded inputs · Every π step source has an unguarded input · Choice selection preserves process scoping · Reduction steps preserve process scoping · Subject reduction for endpoint typing at compatible interfaces

InductiveReduction relation of the π-calculus#✓fully proved

Reduction: communication (substituting the sent channel for the input variable) between any selected output and input guards, reduction under | and ν, and reduction up to structural congruence.

inductive Step : Proc → Proc → Prop
  | commSelect {a : Name} {b : Name} {p' q' p q : Proc} :
      Select p (.out a b p') → Select q (.inp a q') →
      Step (.par p q) (.par p' (subst q' b))
  | parL {p p' q : Proc} : Step p p' → Step (.par p q) (.par p' q)
  | parR {p p' q : Proc} : Step p p' → Step (.par q p) (.par q p')
  | nu {p p' : Proc} : Step p p' → Step (.nu p) (.nu p')
  | cong {p p' q q' : Proc} : Cong p p' → Step p' q' → Cong q' q →
      Step p q

Uses 5 · Used by 77

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

Used byBarbed bisimilar processes have the same barbs · Structural congruence is a strong barbed bisimulation · Every reduction source has an unguarded output · Decorated-LTS bisimulations are exactly strong barbed bisimulations · May-barb after finitely many reductions · Barbed bisimilarity preserves may-barbs · Processes without unguarded output cannot reduce · Reduction LTS decorated with barb observations · Barbed bisimilarity transfers finite reduction paths · Barbed bisimilarity matches each reduction by one reduction · Session communication steps are π-calculus reductions · Session communication paths are π-calculus reduction paths · Progress for balanced ranked guard frontiers · Global progress of ranked processes at balanced interfaces · Closed ranked networks are completed or can step · Reachable states of closed ranked networks stay typed · Progress at reachable states of closed ranked networks · Same-name ranked guards are opposite and communicate · Subject reduction for ranked typing at compatible interfaces · Ranked subject reduction at balanced interfaces · Ranked subject reduction at the empty interface · Reduction preserves the finite linear fragment · Unguarded shared input communicates with a matching output · Every phase of the restricted repeated session can step · Idle processes cannot step · Offered service communicates with a matching shared output · Persistent service offers survive one reduction step · Every phase of the repeated session can step · Every phase is reachable from the pending state · Each phase steps to the next · Declared signature offers survive finite reduction · Service availability survives finite reduction · Sender-invoked state steps by invoking the receiver trigger · Steps preserve typing at the recurring interface · Every round count has a trace returning to the pending state · Repeated-session traces with typing, availability and progress · Repeated-session traces with preserved typing and availability · Pending state steps by invoking the sender trigger · Invoking a replicated service is a reduction step · Session action steps back to the pending state · Every round has a session action on the same endpoint · Declared signature offers survive one reduction step · Service availability survives one reduction step · Arbitrarily long typed repeated-session traces · Typing and compatibility persist along finite executions · Empty-interface typing persists along finite executions · Subject reduction at a compatible conversion interface · Subject reduction at a balanced interface · Subject reduction at the empty interface · Progress for semantically balanced conversion frontiers · Same-name conversion guards are opposite and communicate · Global progress of conversion-ranked processes at balanced interfaces · Finite runs keep conversion ranked typing at compatible interfaces · Reachable closed conversion-ranked states keep the empty interface · Conversion ranked subject reduction at compatible interfaces · Conversion ranked subject reduction at balanced interfaces · Conversion ranked subject reduction at the empty interface · Closed conversion-ranked networks are completed or can step · Progress at reachable states of closed conversion-ranked networks · Exposed shared requests step when declared services are available · Balanced runtime frontiers are idle or step given availability · Global runtime progress at balanced interfaces given availability · Closed runtime processes are idle or step given availability · Multi-step subject reduction at compatible interfaces · Multi-step subject reduction at balanced interfaces · Multi-step subject reduction at the empty interface · Qualified progress at every reachable runtime state · Qualified progress at reachable closed runtime states · Same-name linear guards at a compatible interface communicate · Subject reduction for runtime typing at compatible interfaces · Subject reduction for runtime typing at balanced interfaces · Subject reduction for runtime typing at the empty interface · Every π step source has an unguarded input · Reduction steps preserve process scoping · Subject reduction for endpoint typing at compatible interfaces · Subject reduction for endpoint typing at balanced interfaces · Subject reduction for endpoint typing at the empty interface

13 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.