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
- scientific article; zbMATH DE number 954809 (Why is no real title available?)
- scientific article; zbMATH DE number 42752 (Why is no real title available?)
- A Distributed Pi-Calculus
- A Filter Model for Concurrent $\lambda$-Calculus
- A calculus of mobile processes. II
- A filter lambda model and the completeness of type assignment
- 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 \(\lambda\)-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
- 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 Supports Safe Session Substitution
- Subtyping for session types in the pi calculus
- The \(\pi\)-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
(15)- On the preciseness of subtyping in session types
- Fair termination of multiparty sessions
- Preciseness of subtyping on intersection and union types
- Subtyping Supports Safe Session Substitution
- Interval probability for sessions types
- Preface to the special issue on open problems in concurrency theory
- A Theory of Formal Choreographic Languages
- Communicating finite state machines and an extensible toolchain for multiparty session types
- Denotational and operational preciseness of subtyping: a roadmap. Dedicated to Frank de Boer on the occasion of his 60th birthday
- Composition and decomposition of multiparty sessions
- Precise Subtyping for Asynchronous Multiparty Sessions
- scientific article; zbMATH DE number 7559468 (Why is no real title available?)
- Fair subtyping for multi-party session types
- Deconfined Global Types for Asynchronous Sessions
- scientific article; zbMATH DE number 7327953 (Why is no real title available?)
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)
