Subject reduction for endpoint typing

Unguarded input in a process to Weakening by an unused completed endpoint

• Unguarded input in a process
• Structural congruence preserves unguarded inputs
• Selection reflects unguarded inputs
• Every π step source has an unguarded input
• Absence of a physical name from a process
• An output payload name is not absent
• The inserted name is absent from a lifted process
• Substitution cancels name lifting
• Substitution cancels process lifting
• Injectivity of name lifting
• Name swap is an involution
• Process swap is an involution
• A lifted name is never the innermost binder
• Commuting a name lift past a lift at cutoff zero
• Commutation of name lifts at ordered cutoffs
• Commutation of process lifts at ordered cutoffs
• Lifting preserves and reflects name scoping
• Injectivity of name swapping
• A lifted key is never a freshly bound key
• Weakening by an unused completed endpoint

Weakening by a disjoint completed context to Choice selection preserves process scoping

• Weakening by a disjoint completed context
• Removing a parallel nil preserves endpoint typing
• Extension of a name map under a binder
• Extended name map commutes with lifting outer names
• Capture-safe renaming of processes
• Extending a scoped name map under a binder keeps it scoped
• Extending a lift under a binder raises its cutoff
• Process renaming by a lift is process lifting
• Extending a substitution under a binder raises its cutoff
• Process renaming by a substitution is process substitution
• Capture-safe renaming preserves process scope
• Extending a swap under a binder shifts both indices
• Process renaming by a swap is the restriction swap
• Collision-free renaming preserves endpoint typing
• Binder lifting preserves endpoint typing
• Lifting preserves and reflects process scoping
• Swapping binders in scope preserves name scoping
• Swapping binders in scope preserves process scoping
• Structural congruence preserves process scoping
• Choice selection preserves process scoping

Reduction steps preserve process scoping to Capability whose head is a send with a given continuation

• Reduction steps preserve process scoping
• Endpoint typing drops a role whose name does not occur
• Owned capability with an absent name is completed
• Substitution cancels lifting on endpoint keys
• Received-endpoint substitution is injective when the role is fresh
• 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
• Passive substitution leaves the linear context unchanged
• Passive substitution is injective on lifted outer keys
• Endpoint typing under passive name substitution
• Communicating subjects in a compatible split have dual capabilities
• Dual of a passive send head is a passive receive head
• Passive-payload communication preserves endpoint typing
• Dual of an endpoint send head is an endpoint receive head
• Communicating subjects in a compatible split have equal ranks
• Endpoint-delegating communication preserves typing
• Head communication preserves endpoint typing
• Matched output head of a capability
• Capability whose head is a send with a given continuation

A matched output head is a send with the same continuation to Matching send and receive heads of two capabilities

• A matched output head is a send with the same continuation
• Advancement of a matched dual subject pair
• Head communication preserves typing and records the matched output
• Dual-continuation update leaves other lookups unchanged
• Subject lookup after a dual-continuation update
• Dual advancement preserves the owned keys
• Dual-continuation update preserves compatibility
• Dual advancement preserves compatibility
• Dual-continuation update preserves balance
• Dual advancement preserves balance
• Head communication yields a dual advancement
• Dual advancement preserves disjointness from a frame
• Dual advancement in the left part of a union
• Dual advancement in the right part of a disjoint union
• Swapping two ambient binders in an ownership context
• Binder swapping preserves endpoint typing
• Context swapping commutes with insertion
• Swapping the two innermost binders fixes a twice-lifted context
• Swapping nested restrictions exchanges their bound pairs
• Matching send and receive heads of two capabilities

Semantic advancement of a communicating endpoint pair to Semantic advancement preserves capability ranks

• Semantic advancement of a communicating endpoint pair
• Semantic balance of a linear context
• Semantic balance implies semantic compatibility
• The empty context is semantically balanced
• Raw balance implies semantic balance
• Semantic advancement preserves the context's domain
• Semantic advancement preserves disjointness from a frame
• Semantic advancement preserves scoping of owned keys
• Semantic advancement preserves compatibility
• Semantic advancement preserves balance
• Semantic advancement extends from the left part to the whole union
• Semantic advancement extends from the right part to a disjoint union
• Literally dual capabilities have literally dual continuations
• Communication heads give a send-head observation
• Raw dual advancement is a semantic advancement
• Semantic advancement is raw under literal compatibility
• Lifting preserves semantic advancement
• Binder swapping preserves semantic advancement
• Typed head communication yields a semantic advancement
• Semantic advancement preserves capability ranks

Lowering then lifting an outer key returns it to Endpoint typing is preserved by reverse scope extrusion

• Lowering then lifting an outer key returns it
• Lowering is injective on contexts without fresh-name keys
• Lowering of an outer context past a fresh binder
• Lifting a lowered context recovers it
• Endpoint typing reflects through binder lifting
• Erasing both roles of the fresh name leaves outer keys
• Context lifting is injective
• Lowering preserves disjointness of outer contexts
• Outer insertion commutes with binding a fresh pair
• Updating both bound roles, positive first, rebinds the pair
• Updating both bound roles, negative first, rebinds the pair
• Outer lookups pass through a freshly bound pair
• Dual advancement under restriction splits into inner and outer cases
• Outer dual advancement lifts through restriction
• Dual advancement under restriction splits, keeping the private step
• Inversion of endpoint typing for restriction
• Endpoint typing is preserved by forward scope extrusion
• Endpoint typing absorbs a role absent from its parallel partner
• Endpoint typing restores both bound roles to the restricted side
• Endpoint typing is preserved by reverse scope extrusion

Endpoint typing is invariant under scope extrusion to Binding a fresh dual pair preserves dual compatibility

• Endpoint typing is invariant under scope extrusion
• Parallel commutation preserves endpoint typing
• Parallel reassociation preserves endpoint typing
• Reverse parallel reassociation preserves endpoint typing
• Adding a parallel nil 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
• Structural congruence preserves endpoint typing
• Compatibility restricts to the left part of a union
• Compatibility restricts to the right part of a disjoint union
• Binding a dual private pair preserves compatibility
• Binding a dual private pair preserves balance
• Semantic advance under a private binding is private or outer
• Outer semantic advances lift past a private binding
• Equivalent retyping preserves semantic balance
• Union of disjoint balanced contexts is balanced
• Injective rekeying preserves dual compatibility
• Binding a fresh dual pair preserves dual compatibility

Subject reduction for endpoint typing at compatible interfaces to Subject reduction for endpoint typing at the empty interface

• 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

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.