Session typing up to protocol equivalence
Payload and continuation branches of an endpoint action to Tree equivalence is a congruence for endpoint sending
- Payload and continuation branches of an endpoint action
- Labels of observable protocol-tree edges
- Visible edge of a protocol tree after root unfolding
- Labelled transition system of protocol-tree observations
- Regular-tree equivalence of protocols as bisimilarity
- Protocol tree equivalence is reflexive
- Protocol tree equivalence is symmetric
- Protocol tree equivalence is transitive
- Root unfolding preserves protocol-tree edges
- A protocol is tree-equivalent to its unfolding
- Head and branch matching of protocols up to a child relation
- Head matching is monotone in the child relation
- Head-matching relations are bisimulations
- Tree-equivalent protocols have matching heads
- Coinduction principle for protocol tree equivalence
- Characterization of tree equivalence by matching heads
- Unfolding both protocols preserves and reflects tree equivalence
- Tree equivalence is a congruence for name sending
- Tree equivalence is a congruence for name receiving
- Tree equivalence is a congruence for endpoint sending
Tree equivalence is a congruence for endpoint receiving to Conversion-typed processes are well scoped
- Tree equivalence is a congruence for endpoint receiving
- Head matching transfers to dual protocols
- Duality preserves protocol tree equivalence
- Duality preserves and reflects protocol tree equivalence
- Protocol tree equivalence is an equivalence relation
- Tree equivalence of endpoint sends, componentwise
- Tree equivalence of endpoint receives, componentwise
- Tree equivalence preserves completion of a protocol
- Equivalence of endpoint capabilities
- Reflexivity of capability equivalence
- Symmetry of capability equivalence
- Transitivity of capability equivalence
- Duality preserves capability equivalence
- 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
- Conversion-typed processes are well scoped
Conversion-typed processes have no sum or replication to Peer of a passive send head has an equivalent receive head
- Conversion-typed processes have no sum or replication
- Parallel inversion for conversion typing
- Restriction inversion for conversion typing
- Nil inversion for conversion typing
- Typed nil admits a completed scoped capability
- Weakening conversion typing by a completed capability
- Weakening conversion typing by a disjoint completed context
- Removing a parallel nil preserves conversion typing
- Erasing a role with an absent name preserves typing
- Owned capabilities with absent names are completed
- Retyping along ownership-map equivalence
- Ownership-map equivalence preserves typing in both directions
- Collision-free renaming preserves conversion typing
- Lifting past a binder preserves conversion typing
- Swapping adjacent binders preserves conversion typing
- Endpoint substitution preserves conversion typing
- Endpoint substitution with freshness from a disjoint split
- Passive name substitution preserves conversion typing
- Communicating subjects have semantically dual capabilities
- Peer of a passive send head has an equivalent receive head
Peer of an endpoint send head has an equivalent receive head to Swapping nested restrictions preserves conversion typing
- Peer of an endpoint send head has an equivalent receive head
- Input inversion for conversion typing
- Passive head communication preserves conversion typing
- Endpoint delegation preserves conversion typing
- Head update leaves other lookups unchanged
- Head communication preserves conversion typing
- Head update leaves the transmitted payload slot unchanged
- Lowering a lifted process preserves conversion typing
- Forward scope extrusion preserves conversion typing
- Adding a role unused by the partner preserves conversion typing
- Restoring the bound pair to the restricted component
- Reverse scope extrusion preserves conversion typing
- Scope extrusion preserves conversion typing in both directions
- Parallel commutation preserves conversion typing
- Parallel reassociation preserves conversion typing
- Reverse parallel reassociation preserves conversion typing
- Adding a parallel nil 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
Reverse restriction swap preserves conversion typing to Erasing a key whose name is absent preserves conversion ranked typing
- Reverse restriction swap preserves conversion typing
- Structural congruence preserves conversion typing
- Subject reduction at a compatible conversion interface
- Subject reduction at a balanced interface
- Subject reduction at the empty interface
- Typing and compatibility persist along finite executions
- Empty-interface typing persists along finite executions
- Priority-ranked conversion typing judgement
- Forgetting priorities yields conversion typing
- Ranked typing embeds into conversion ranked typing
- Parallel inversion for conversion ranked typing
- Restriction inversion for conversion ranked typing
- Nil typing lifts to conversion ranked typing
- Conversion-ranked output subjects are active
- Conversion-ranked input subjects are active
- Minimum active role is the subject of a conversion frontier leaf
- Completed conversion-ranked frontiers are congruent to nil
- Minimum guard leaf cannot own an equivalent dual peer
- Weakening conversion ranked typing by a completed capability
- Erasing a key whose name is absent preserves conversion ranked typing
Weakening conversion ranked typing by a disjoint completed context to Adding a role unused by the partner preserves conversion ranked typing
- Weakening conversion ranked typing by a disjoint completed context
- Equivalent contexts preserve the guard condition
- Equivalent contexts preserve conversion ranked typing
- Context equivalence transports conversion ranked typing both ways
- Collision-free renaming preserves conversion ranked typing
- Binder lifting preserves conversion ranked typing
- Binder swap preserves conversion ranked typing
- Endpoint substitution preserves conversion ranked typing
- Split-derived freshness for conversion endpoint substitution
- Passive substitution preserves conversion ranked typing
- Inversion of conversion-ranked input typing
- Passive head communication preserves conversion ranked typing
- Endpoint head communication preserves conversion ranked typing
- Head preservation for a conversion-ranked opposite pair
- Conversion head communication yields a semantic advance
- Same-name conversion guards are opposite and communicate
- Progress for semantically balanced conversion frontiers
- Conversion ranked typing descends from a lifted process
- Forward scope extrusion preserves conversion ranked typing
- Adding a role unused by the partner preserves conversion ranked typing
Restoring the bound pair preserves conversion ranked typing to Global progress of conversion-ranked processes at balanced interfaces
- Restoring the bound pair preserves conversion ranked typing
- Reverse scope extrusion preserves conversion ranked typing
- Conversion ranked typing is invariant under scope extrusion
- Parallel commutation preserves conversion ranked typing
- Parallel reassociation preserves conversion ranked typing
- Reverse parallel reassociation preserves conversion ranked typing
- Removing a parallel nil preserves conversion ranked typing
- Adding a parallel nil preserves conversion ranked typing
- 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
- Structural congruence 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
- Finite runs keep conversion ranked typing at compatible interfaces
- Reachable closed conversion-ranked states keep the empty interface
- Conversion-ranked processes have a typed frontier normal form
- Global progress of conversion-ranked processes at balanced interfaces
Closed conversion-ranked networks are completed or can step to Progress at reachable states of closed conversion-ranked networks
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.