Precise subtyping for synchronous multiparty sessions
From MaRDI portal
Abstract: The notion of subtyping has gained an important role both in theoretical and applicative domains: in lambda and concurrent calculi as well as in programming languages. The soundness and the completeness, together referred to as the preciseness of subtyping, can be considered from two different points of view: operational and denotational. The former preciseness has been recently developed with respect to type safety, i.e. the safe replacement of a term of a smaller type when a term of a bigger type is expected. The latter preciseness is based on the denotation of a type which is a mathematical object that describes the meaning of the type in accordance with the denotations of other expressions from the language. The result of this paper is the operational and denotational preciseness of the subtyping for a synchronous multiparty session calculus. The novelty of this paper is the introduction of characteristic global types to prove the operational completeness.
Recommendations
- On the preciseness of subtyping in session types
- Preciseness of subtyping on intersection and union types
- Fair subtyping for multi-party session types
- Subtyping for session types in the pi calculus
- Denotational and operational preciseness of subtyping: a roadmap. Dedicated to Frank de Boer on the occasion of his 60th birthday
Cites work
- A calculus of mobile processes. II
- A Distributed Pi-Calculus
- A filter lambda model and the completeness of type assignment
- A Filter Model for Concurrent \lambda-Calculus
- A gentle introduction to multiparty asynchronous session types
- A semantic deconstruction of session types
- Automata, Languages and Programming
- Barbed bisimulation
- Completeness of intersection and union type assignment systems for call-by-value -models
- Computer Science Logic
- Denotational and operational preciseness of subtyping: a roadmap. Dedicated to Frank de Boer on the occasion of his 60th birthday
- Full abstraction in a subtyped pi-calculus with linear types
- Global Principal Typing in Partially Commutative Asynchronous Sessions
- Global progress for dynamically interleaved multiparty sessions
- Globally Governed Session Semantics
- Globally governed session semantics
- scientific article; zbMATH DE number 954809 (Why is no real title available?)
- scientific article; zbMATH DE number 42752 (Why is no real title available?)
- Multiparty asynchronous session types
- Multiparty Asynchronous Session Types
- On reduction-based process semantics
- 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
- Parameterised Multiparty Session Types
- Parameterised multiparty session types
- Preciseness of subtyping on intersection and union types
- Semantic subtyping for the pi-calculus
- Semantic subtyping, dealing set-theoretically with function, union, intersection, and negation types
- Sub-behaviour relations for session-based client/server systems
- Subtyping for session types in the pi calculus
- Subtyping Supports Safe Session Substitution
- The -calculus: A theory of mobile processes
- The completeness theorem for typing lambda-terms
- Types and programing languages
- Undecidability of asynchronous session subtyping
- Using higher-order contracts to model session types
Cited in
(23)- Composition and decomposition of multiparty sessions
- Denotational and operational preciseness of subtyping: a roadmap. Dedicated to Frank de Boer on the occasion of his 60th birthday
- Preface to the special issue on open problems in concurrency theory
- Communicating finite state machines and an extensible toolchain for multiparty session types
- Subtyping Supports Safe Session Substitution
- scientific article; zbMATH DE number 7559468 (Why is no real title available?)
- Preciseness of subtyping on intersection and union types
- On the preciseness of subtyping in session types
- Fair subtyping for multi-party session types
- scientific article; zbMATH DE number 7327953 (Why is no real title available?)
- Deconfined Global Types for Asynchronous Sessions
- Precise Subtyping for Asynchronous Multiparty Sessions
- Interval probability for sessions types
- A Theory of Formal Choreographic Languages
- Fair termination of multiparty sessions
- Completeness of asynchronous session tree subtyping in Coq
- A sound and complete projection for global types
- Separation and encodability in mixed choice multiparty sessions
- Crash-stop failures in asynchronous multiparty session types
- Less is more revisited: association with global protocols and multiparty sessions
- Certified implementability of global multiparty protocols
- Formalising subject reduction and progress for multiparty session processes
- Formalising asynchronous session subtyping
This page was built for publication: Precise subtyping for synchronous multiparty sessions
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2423747)
