Ilaria Castellani, Mariangiola Dezani-Ciancaglini, Paola Giannini
We propose an interpretation of multiparty sessions as "flow event structures", which allows concurrency between communications within a session to be explicitly represented. We show that this interpretation is equivalent, when the multiparty sessions can be described by global types, to an interpretation of global types as "prime event structures".
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
Multiparty sessions are systems of concurrent processes, which allow several participants to communicate by sending and receiving messages. Their overall behaviour can be described by means of global types. Typable multiparty session enjoy lock-freedom. We look at multiparty sessions as open systems by a suitable definition of connection transforming compatible processes into gateways (forwarders). A relation resembling the standard subtyping relation for session types is used to formalise compatibility. We show that the session obtained by connection can be typed by manipulating the global ty…
Asynchronous Multiparty Sessions with Mixed Choice
本文提出一种异步多方会话的校验算法，支持输入和输出前缀的非确定性选择，通过全局类型系统确保通信标签集的连贯性，证明了类型正确性和会话保真性，展示了混合选择在异步多方协议中的表达力。
Global types and event structure semantics for asynchronous multiparty sessions
本文提出将异步通信的多方会话解释为流事件结构，并引入新的全局类型概念，确保会话的预期属性，如进展。全局类型通过更直接地反映异步性并更宽松地解释为原始事件结构。
Partially Typed Multiparty Sessions
针对标准类型系统无法为部分含可忽略通信的多方会话做类型标注的问题，提出满足主体归约、会话保真度与部分无锁性的类型系统，并给出可靠完备的类型推断算法。
Reversible interactions model different scenarios, like biochemical systems and human as well as automatic negotiations. We abstract interactions via multiparty sessions enriched with named checkpoints. Computations can either go forward or roll back to some checkpoints, where possibly different choices may be taken. In this way communications can be undone and different conversations may be tried. Interactions are typed with global types, which control also rollbacks. Typeability of session participants in agreement with global types ensures session fidelity and progress of reversible communi…
Partial Typing for Asynchronous Multiparty Sessions
本文针对并发系统验证难以局部化的问题，提出异步多方会话的部分类型指派系统，并证明其可类型性保证部分锁自由与孤儿消息自由。
Modular Multiparty Sessions with Mixed Choice
本文提出一种面向多方会话的类型指派方法，将混合选择限制在松散耦合模块内部使用，从而在提升表达能力的同时保证主体归约、会话保真性和无锁性。
This paper presents the first formalisation of the precise subtyping relation for asynchronous multiparty sessions. We show that our subtyping relation is sound (i.e., guarantees safe process replacement) and also complete: any extension of the relation is unsound. To achieve our results, we develop a novel session decomposition technique, from full session types (including internal/external choices) into single input/output session trees (without choices). Previous work studies precise subtyping for binary sessions (with just two participants), or multiparty sessions (with any number of parti…
Separation and Encodability in Mixed Choice Multiparty Sessions (Technical Report)
本文为混合选择同步多方会话演算提出通用类型系统并证明其安全性，进而通过可编码性与分离性分析比较九个演算的表达能力，证明MCMP严格强于经典多方会话。
FTMPST: Fault-Tolerant Multiparty Session Types
本文扩展多方会话类型以集成容错机制，应对不可靠通信和进程崩溃等系统故障，并通过故障模式增强进程语义，成功应用于分析Chandra和Toueg的旋转协调器算法变体。
For many application-level distributed protocols and parallel algorithms, the set of participants, the number of messages or the interaction structure are only known at run-time. This paper proposes a dependent type theory for multiparty sessions which can statically guarantee type-safe, deadlock-free multiparty interactions among processes whose specifications are parameterised by indices. We use the primitive recursion operator from Gödel's System T to express a wide range of communication patterns while keeping type checking decidable. To type individual distributed processes, a parameteris…
Relating the specification of the global communication behavior of a distributed system and the specifications of the local communication behavior of each of its nodes/peers (e.g., to check if the former is realizable by the latter under some safety and/or liveness conditions) is a challenging problem addressed in many relevant scenarios. In the context of networked software services, a widespread programming language-based approach relies on global specifications defined by session types or behavioral contracts. Static type checking can then be used to ensure that components follow the prescr…
The additional complexity caused by concurrently communicating processes in distributed systems render the verification of such systems into a very hard problem. Multiparty session types were developed to govern communication and concurrency in distributed systems. As such, they provide an efficient verification method w.r.t. properties about communication and concurrency, like communication safety or progress. However, they do not support the analysis of properties that require the consideration of concrete runs or concrete values of variables. We sequentialise well-typed systems of processes…
On Asynchronous Multiparty Session Types for Federated Learning
本文改进了会话类型理论，以支持建模和验证实现联邦学习协议的过程。通过引入面向多个参与者的输入/输出操作，增强了灵活性并允许安全的过程替换。
We interpret Linear Logic Proof Nets in a term language based on Solos calculus. The system includes a synchronisation mechanism, obtained by a conservative extension of the logic, that enables to define non-deterministic behaviours and multiparty sessions.
Formally Verified Liveness with Multiparty Session Types in Rocq
本文在Rocq证明助手中首次机械化证明了同步多方会话类型的活性，利用共归纳树和子类型关系建立局部类型与全局类型的操作对应，从而保证会话的安全性和活性。
There exists a broad family of multiparty sessions in which the progress of one session participant is not unconditional, but depends on the choices performed by other participants. These sessions fall outside the scope of currently available session type systems that guarantee progress. In this work we propose the first type system ensuring that well-typed multiparty sessions, including those exhibiting the aforementioned dependencies, fairly terminate. Fair termination is termination under a fairness assumption that disregards those interactions deemed unfair and therefore unrealistic. Fair …
A Logical Interpretation of Asynchronous Multiparty Compatibility
本文在命题即类型框架下将多方兼容性的相干性条件推广为转发器，并证明转发器完全刻画所有类型良好的多方兼容进程。
In this paper we introduce imprecise probability for session types. More exactly, we use a probabilistic process calculus in which both nondeterministic external choice and probabilistic internal choice are considered. We propose the probabilistic multiparty session types able to codify the structure of the communications by using some imprecise probabilities given in terms of lower and upper probabilities. We prove that this new probabilistic typing system is sound, as well as several other results dealing with both classical and probabilistic properties. The approach is illustrated by a simp…
Multiparty session calculi have been recently equipped with security requirements, in order to guarantee properties such as access control and leak freedom. However, the proposed security requirements seem to be overly restrictive in some cases. In particular, a party is not allowed to communicate any kind of public information after receiving a secret information. This does not seem justified in case the two pieces of information are totally unrelated. The aim of the present paper is to overcome this restriction, by designing a type discipline for a simple multiparty session calculus, which c…
We identify multirole logic as a new form of logic and formalize linear multirole logic (LMRL) as a natural generalization of classical linear logic (CLL). Among various meta-properties established for LMRL, we obtain one named multi-cut elimination stating that every cut between three (or more) sequents (as a generalization of a cut between two sequents) can be eliminated, thus extending the celebrated result of cut-elimination by Gentzen. We also present a variant of $π$-calculus for multiparty sessions that demonstrates a tight correspondence between process communication in this variant an…
Session types enable the specification and verification of communicating systems. However, their theory often assumes that processes never fail. To address this limitation, we present a generalised multiparty session type (MPST) theory with crash-stop failures, where processes can crash arbitrarily. Our new theory validates more protocols and processes w.r.t. previous work. We apply minimal syntactic changes to standard session π-calculus and types: we model crashes and their handling semantically, with a generalised MPST typing system parametric on a behavioural safety property. We cover the …
Mixed Choice Multiparty Session Types, Precisely
本文针对含会话委托等特性的混合选择多方会话类型，证明其子类型关系的精确性，开发通用类型系统并实现相关检查算法，经案例研究验证其有效性。
We develop a generalization of existing Curry-Howard interpretations of (binary) session types by relying on an extension of linear logic with features from hybrid logic, in particular modal worlds that indicate domains. These worlds govern domain migration, subject to a parametric accessibility relation familiar from the Kripke semantics of modal logic. The result is an expressive new typed process framework for domain-aware, message-passing concurrency. Its logical foundations ensure that well-typed processes enjoy session fidelity, global progress, and termination. Typing also ensures that …
This paper proposes a bisimulation theory based on multiparty session types where a choreography specification governs the behaviour of session typed processes and their observer. The bisimulation is defined with the observer cooperating with the observed process in order to form complete global session scenarios and usable for proving correctness of optimisations for globally coordinating threads and processes. The induced bisimulation is strictly more fine-grained than the standard session bisimulation. The difference between the governed and standard bisimulations only appears when more tha…
Compositional Interface Refinement Through Subtyping in Probabilistic Session Types
本文提出概率混合选择多方会话π演算及其灵活子类型系统，允许用多个通道细化单个接口，并证明主体归约、无错误性和无死锁性，从而支持概率分布式通信的组合式验证与逐步细化。
Fault-Tolerant Multiparty Session Types with Global Escape Loops
该研究扩展了带故障模式的容错多方会话类型FTMPST，新增无需全局协调、带非阻塞退出消息的全局跳出容错循环结构，并通过旋转协调器算法变体验证了方法的可行性，为容错分布式算法的属性验证提供支持。
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…
We propose a calculus for asynchronous multiparty sessions where input choices with different senders are allowed in processes. We present a type system that accepts such input races provided they do not hinder lock-freedom.
Towards Multiparty Session Types for Highly-Concurrent and Fault-Tolerant Web Applications
本文提出一种全局类型框架，为多方会话类型添加显式失败语义和动态参与，以支持高并发和容错Web应用的正式验证。
Crash-Stop Failures in Asynchronous Multiparty Session Types
针对现实分布式系统中的崩溃故障，提出一种带崩溃停止语义的异步多参与方会话类型理论，通过崩溃处理分支和可选可靠性假设，保证良类型进程的无死锁、协议一致性与活性。
We present Multiparty Classical Choreographies (MCC), a language model where global descriptions of communicating systems (choreographies) implement typed multiparty sessions. Typing is achieved by generalising classical linear logic to judgements that explicitly record parallelism by means of hypersequents. Our approach unifies different lines of work on choreographies and processes with multiparty sessions, as well as their connection to linear logic. Thus, results developed in one context are carried over to the others. Key novelties of MCC include support for server invocation in choreogra…
This paper deals with the probabilistic behaviours of distributed systems described by a process calculus considering both probabilistic internal choices and nondeterministic external choices. For this calculus we define and study a typing system which extends the multiparty session types in order to deal also with probabilistic behaviours. The calculus and its typing system are motivated and illustrated by a running example.
Causal Consistency for Reversible Multiparty Protocols
本文扩展了基于监视器即记忆的方法，为支持多方协议、异步通信、解耦回滚和抽象传递的进程模型定义了可逆语义，并证明了该语义具有因果一致性。
Session types define protocols that processes must follow when communicating. The special case of binary session types, i.e. type annotations of protocols between two parties, is known to be in a propositions-as-types correspondence with linear logic. In previous work, we have shown that the generalization to multiparty session types can be expressed either by coherence proofs or by arbiters, processes that act as middleware by forwarding messages according to the given protocol. In this paper, following the propositions-as-types fashion, we generalize arbiters to a logic, which we call forwar…
Recent work on the enhancement of multiparty session types with logical annotations enable the effective verification of properties on (1) the structure of the conversations, (2) the sorts of the messages, and (3) the actual values exchanged. In [3] we extend this work to enable the specification and verification of mutual effects of multiple cross-session interactions. Here we give a sound and complete embedding into the Hennessy-Milner logic to justify the expressiveness of the approach in [3] and to provide it with a logical background that will enable us to compare it with similar approach…
Protocols provide the unifying glue in concurrent and distributed software today; verifying that message-passing programs conform to such governing protocols is important but difficult. Static approaches based on multiparty session types (MPST) use protocols as types to avoid protocol violations and deadlocks in programs. An elusive problem for MPST is to ensure both protocol conformance and deadlock freedom for implementations with interleaved and delegated protocols. We propose a decentralized analysis of multiparty protocols, specified as global types and implemented as interacting processe…
The paper presents a data-driven model of self-adaptivity for multiparty sessions. System choreography is prescribed by a global type. Participants are incarnated by processes associated with monitors, which control their behaviour. Each participant can access and modify a set of global data, which are able to trigger adaptations in the presence of critical changes of values. The use of the parallel composition for building global types, monitors and processes enables a significant degree of flexibility: an adaptation step can dynamically reconfigure a set of participants only, without alterin…
Deconfined Global Types for Asynchronous Sessions
本文提出一种改进的异步多参与者会话类型系统，在满足良构条件时保留主体归约、会话保真和进展性质，并配有健全完备的类型推断算法，通过检查良构条件的受限形式恢复类型化的有效性。
We present a process algebra aimed at describing interactions that are multiparty, i.e. that may involve more than two processes and that are open, i.e. the number of the processes they involve is not fixed or known a priori. Here we focus on the theory of a core version of a process calculus, without message passing, called Core Network Algebra (CNA). In CNA communication actions are given not in terms of channels but in terms of chains of links that record the source and the target ends of each hop of interactions. The operational semantics of our calculus mildly extends the one of CCS. The …
Correctly Communicating Software: Distributed, Asynchronous, and Beyond (extended version)
本论文以会话类型的逻辑基础为核心，研究如何在保证正确性的前提下扩展二元与多方会话类型的表达力及适用范围，以支撑分布式异步消息传递软件的可靠验证。
We study an urgent semantics of asynchronous timed session types, where input actions happen as soon as possible. We show that with this semantics we can recover to the timed setting an appealing property of untimed session types: namely, deadlock-freedom is preserved when passing from synchronous to asynchronous communication.
In the setting of the pi-calculus with binary sessions, we aim at relaxing the notion of duality of session types by the concept of retractable compliance developed in contract theory. This leads to extending session types with a new type operator of "speculative selection" including choices not necessarily offered by a compliant partner. We address the problem of selecting successful communicating branches by means of an operational semantics based on orchestrators, which has been shown to be equivalent to the retractable semantics of contracts, but clearly more feasible. A type system, sound…
Session types are types for specifying protocols that processes must follow when communicating with each other. Session types are in a propositions-as-types correspondence with linear logic. Previous work has shown that a multiparty session type, a generalisation of session types to protocols of two or more parties, can be modelled as a proof of coherence, a generalisation of linear logic duality. And, protocols expressed as coherence can be simulated by arbiters, processes that act as a middleware by forwarding messages according to the given protocol. In this paper, we generalise the concept…
Towards a Semantic Characterisation of Global Type Well-formedness
本文以素事件结构为语义模型，为多方会话全局类型的可投影性和有界性提供语义刻画，并识别出良构全局类型对应PES的结构性质。
We investigate how different fairness assumptions affect results concerning lock-freedom, a typical liveness property targeted by session type systems. We fix a minimal session calculus and systematically take into account all known fairness assumptions, thereby identifying precisely three interesting and semantically distinct notions of lock-freedom, all of which having a sound session type system. We then show that, by using a general merge operator in an otherwise standard approach to global session types, we obtain a session type system complete for the strongest amongst those notions of l…
We present Concurrent GV (CGV), a functional calculus with message-passing concurrency governed by session types. With respect to prior calculi, CGV has increased support for concurrent evaluation and for cyclic network topologies. The design of CGV draws on APCP, a session-typed asynchronous pi-calculus developed in prior work. Technical contributions are (i) the syntax, semantics, and type system of CGV; (ii) a correct translation of CGV into APCP; (iii) a technique for establishing deadlock-free CGV programs, by resorting to APCP's priority-based type system.
We present Concurrent GV (CGV), a functional calculus with message-passing concurrency governed by session types. With respect to prior calculi, CGV has increased support for concurrent evaluation and for cyclic network topologies. The design of CGV draws on APCP, a session-typed asynchronous pi-calculus developed in prior work. Technical contributions are (i) the syntax, semantics, and type system of CGV; (ii) a correct translation of CGV into APCP; (iii) a technique for establishing deadlock-free CGV programs, by resorting to APCP's priority-based type system.
Up to now session types have been used under the assumptions of point to point communication, to ensure the linearity of session endpoints, and reliable communication, to ensure send/receive duality. In this paper we define a session type theory for broadcast communication semantics that by definition do not assume point to point and reliable communication. Our session framework lies on top of the parametric framework of broadcasting psi-calculi, giving insights on developing session types within a parametric framework. Our session type theory enjoys the properties of soundness and safety. We …
Much research has studied foundations for correct and reliable communication-centric systems. A salient approach to correctness uses session types to enforce structured communications; a recent approach to reliability uses reversible actions as a way of reacting to unanticipated events or failures. This note develops a simple observation: the machinery required to define asynchronous semantics and monitoring can also support reversible protocols. We propose a process framework of session communication in which monitors support reversibility. A key novelty in our approach are session types with…
Concurrent C0 is an imperative programming language in the C family with session-typed message-passing concurrency. The previously proposed semantics implements asynchronous (non-blocking) output; we extend it here with non-blocking input. A key idea is to postpone message reception as much as possible by interpreting receive commands as a request for a message. We implemented our ideas as a translation from a blocking intermediate language to a non-blocking language. Finally, we evaluated our techniques with several benchmark programs and show the results obtained. While the abstract measure …
This paper builds on prior work investigating the adaptation of session types to provide behavioural information about Elixir modules. A type system called ElixirST has been constructed to statically determine whether functions in an Elixir module observe their endpoint specifications, expressed as session types; a corresponding tool automating this typechecking has also been constructed. In this paper we formally validate this type system. An LTS-based operational semantics for the language fragment supported by the type system is developed, modelling its runtime behaviour when invoked by the…
We present an extension of System F with higher-order context-free session types. The mixture of functional types with session types has proven to be a challenge for type equivalence formalization: whereas functional type equivalence is often rule-based, session type equivalence usually follows a semantic approach based on bisimulations. We propose a unifying approach that handles the equivalence of functional and session types together. We present three notions of type equivalence: a syntactic rule-based version, a semantic bisimulation-based version, and an algorithmic version by reduction t…
A Logical Account of Subtyping for Session Types
本文在带不动点的线性逻辑框架下研究会话类型的子类型关系，提出一种同时保持安全性与终止性的子类型刻画，并证明该子类型在理论上可通过强制语义编译消除。
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈
发表机构由 AI 从论文文本抽取，如发现错误，欢迎反馈修正建议。