Completeness of asynchronous session tree subtyping in Coq
From MaRDI portal
Cites work
- \textbf{Actris 2.0}: asynchronous session-type based reasoning in separation logic
- A formal theory of choreographic programming
- A higher-order logic for concurrent termination-preserving refinement
- A sound and complete projection for global types
- Fair refinement for asynchronous session types
- Full abstraction in a subtyped pi-calculus with linear types
- scientific article; zbMATH DE number 7327953 (Why is no real title available?)
- Kalas: a verified, end-to-end compiler for a choreographic language
- Linear type theory for asynchronous session types
- Nested protocols in session types
- On Communicating Finite-State Machines
- On the boundary between decidability and undecidability of asynchronous session subtyping
- On the preciseness of subtyping in session types
- On the undecidability of asynchronous session subtyping
- Precise Subtyping for Asynchronous Multiparty Sessions
- Precise subtyping for synchronous multiparty sessions
- Subtyping for session types in the pi calculus
- The power of parameterization in coinductive proof
- Undecidability of asynchronous session subtyping
Cited in
(4)
This page was built for publication: Completeness of asynchronous session tree subtyping in Coq
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6860020)
