Session typing with shared services

Shared service signature to Idleness is invariant under structural congruence

• Shared service signature
• Shared service environment
• Separation of owned linear names from shared names
• Priority of a shared invocation over active owned keys
• Empty ownership is separated from shared names
• Singleton context with a nonshared name is separated
• Invocation priority for a singleton of rank above the priority
• Structural shared-service template
• Service templates are invariant under lifting
• Service templates are invariant under binder swapping
• Service templates are invariant under structural congruence
• Unguarded shared input on a given name
• Structural congruence preserves unguarded shared inputs
• Persistent service offer on a given name
• Offered services have an unguarded shared input
• Structural congruence preserves persistent service offers
• Declared persistent service offer
• Idle process as a structural service template
• Declared service offers are invariant under congruence
• Idleness is invariant under structural congruence

Name map fixing every declared shared constant to Inserting a nonshared key preserves separation

• Name map fixing every declared shared constant
• Nonaliasing of owned-name images with shared constants
• Binder extension preserves fixing of shared constants
• Rekeying along a nonaliasing name map yields separation
• Erasing an owned key preserves nonaliasing
• Updating an already-owned key preserves nonaliasing
• Every name map is nonaliasing on empty ownership
• Binder extension preserves nonaliasing of lifted contexts
• Nonaliasing survives adding a received parameter under a binder
• Nonaliasing survives binding a private session pair
• Nonaliasing restricts to the left part of a union
• Nonaliasing restricts to the right part of a union
• Service templates are preserved by renamings fixing shared names
• Rekeying preserves shared invocation priority
• Rekeying the empty context gives the empty context
• Rekeying a singleton moves its key and keeps its capability
• Separation gives nonaliasing for binder lifting
• Separation gives nonaliasing for binder swapping
• Erasing an owned key preserves separation
• Inserting a nonshared key preserves separation

Binder lifting preserves separation to Inversion of runtime typing for input on a shared name

• Binder lifting preserves separation
• Binding a private pair preserves separation
• Separation restricts to the left part of a union
• Separation restricts to the right part of a disjoint union
• Runtime typing with guarded shared replication
• Finite ranked typing embeds into runtime typing under separation
• Extension of a shared service environment
• Service templates survive environment extension
• Environment extension preserves runtime typing under separation
• Runtime typing separates owned names from shared services
• Replicated runtime processes have completed ownership
• Typed replication has a body with empty ownership
• Runtime-typed processes are scoped at the ambient depth
• Typing rule for a replicated input on a shared name
• Inversion of runtime typing for the nil process
• Inversion of runtime typing for parallel composition
• Inversion of runtime typing for restriction
• Output subjects are owned endpoints or declared shared names
• Output on a declared shared name is a service invocation
• Inversion of runtime typing for input on a shared name

Inversion of runtime typing for replication to Adding a restriction around nil preserves runtime typing

• Inversion of runtime typing for replication
• Inversion of runtime typing for a replicated shared input
• Typed replicated shared inputs are offered services
• Inserting a completed entry preserves invocation priority
• Weakening runtime typing by one fresh completed entry
• Weakening runtime typing by a disjoint completed context
• Erasing an owned key preserves invocation priority
• Owned names absent from a runtime process are completed
• Erasing a key whose name is absent preserves runtime typing
• Equivalent retyping preserves separation from shared names
• Equivalent retyping preserves invocation priority
• Runtime typing transfers to an equivalent linear context
• Runtime typing is invariant under equivalent linear contexts
• Each owned key of a runtime typing is scoped at ambient depth
• Whole owned context of a runtime typing is scoped at ambient depth
• Typed service templates own only completed entries
• Typed service templates retype at any well-formed completed context
• Typed service templates retype at empty ownership
• Removing a restriction around nil preserves runtime typing
• Adding a restriction around nil preserves runtime typing

Runtime typing under renamings that fix and avoid shared names to Request-freeness is invariant under binder swapping

• Runtime typing under renamings that fix and avoid shared names
• Binder lifting preserves runtime typing
• Binder swapping preserves runtime typing
• Nonshared endpoint substitution keeps owned names nonshared
• Passive substitution creates no owned shared-name alias
• Runtime typing under substitution of a transmitted endpoint
• Runtime typing under passive name substitution
• Endpoint substitution with side conditions derived from a split
• Runtime typing reflects through binder lifting
• Runtime typing is preserved by forward scope extrusion
• Runtime typing absorbs a role absent from its parallel partner
• Runtime typing restores both bound roles to the restricted side
• Runtime typing is preserved by reverse scope extrusion
• Runtime typing is invariant under scope extrusion
• Structural congruence preserves runtime typing
• Guarded frontier of guards and idle service templates
• Guarded normal form: restrictions over a guarded frontier
• Process with no exposed output on a declared shared name
• Request-freeness is invariant under lifting
• Request-freeness is invariant under binder swapping

Request-freeness is invariant under structural congruence to Runtime head communication advances or keeps the interface

• Request-freeness is invariant under structural congruence
• Service templates are request-free
• Lifting preserves guarded frontiers
• Lifting preserves guarded normal forms
• Parallel composition preserves guarded normal forms up to congruence
• Runtime-typed processes are congruent to a guarded normal form
• Guarded normal form of a typed process keeps its typing
• Request-free runtime outputs have an active linear subject
• Runtime inputs are active linear or have completed ownership
• Request-free completed runtime frontiers are service templates
• Minimum active key is the subject of a runtime frontier leaf
• Runtime minimum guard leaf cannot own an equivalent dual peer
• Non-request-free frontier exposes a shared output up to congruence
• Exposed shared requests step when declared services are available
• Shared invocation and input worker preserve the combined interface
• Inversion of runtime input on a nonshared subject
• Semantic advance preserves shared-linear separation
• Passive head communication preserves runtime typing
• Endpoint head communication preserves runtime typing
• Runtime head communication advances or keeps the interface

Same-name linear guards at a compatible interface communicate to Qualified progress at reachable closed runtime states

• Same-name linear guards at a compatible interface communicate
• Balanced runtime frontiers are idle or step given availability
• 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
• Multi-step subject reduction at compatible interfaces
• Multi-step subject reduction at balanced interfaces
• Multi-step subject reduction at the empty interface
• Global runtime progress at balanced interfaces given availability
• Closed runtime processes are idle or step given availability
• Qualified progress at every reachable runtime state
• Qualified progress at reachable closed runtime states

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.