Simon J. Gay, Peter Thiemann, Vasco T. Vasconcelos
Duality is a central concept in the theory of session types. Since a flaw was found in the original definition of duality for recursive types, several other definitions have been published. As their connection is not obvious, we compare the competing definitions, discuss tradeoffs, and prove some equivalences. Some of the results are mechanized in Agda.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
Multiparty Session Types (MPST) are a well-established typing discipline for message-passing processes interacting on sessions involving two or more participants. Session typing can ensure desirable properties: absence of communication errors and deadlocks, and protocol conformance. However, existing MPST works provide a subject reduction result that is arguably (and sometimes, surprisingly) restrictive: it only holds for typing contexts with strong duality constraints on the interactions between pairs of participants. Consequently, many "intuitively correct" examples cannot be typed and/or ca…
The fast growth of service-oriented programming (SOP) is evident in this day and age of the Internet, and handling communication is of paramount importance in SOP. Session types are a formalism that is proposed to specify interactions between communicating processes. In essence, a session type system is a kind of type system designed to enforce (through type-checking) that the involved processes communicate according to a chosen protocol specified as a session type. It is well-known that linear logic plays a pivotal role in the study of session types. For instance, various inference rules in l…
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 model structured communication-based programming. In particular, binary session types for the pi-calculus describe communication between exactly two participants in a distributed scenario. Adding sessions to the pi-calculus means augmenting it with type and term constructs. In a previous paper, we tried to understand to which extent the session constructs are more complex and expressive than the standard pi-calculus constructs. Thus, we presented an encoding of binary session pi-calculus to the standard typed pi-calculus by adopting linear and variant types and the continuation-p…
Session types offer a type-based discipline for enforcing communication protocols in distributed programming. We have previously formalized simple session types in the setting of multi-threaded $λ$-calculus with linear types. In this work, we build upon our earlier work by presenting a form of dependent session types (of DML-style). The type system we formulate provides linearity and duality guarantees with no need for any runtime checks or special encodings. Our formulation of dependent session types is the first of its kind, and it is particularly suitable for practical implementation. As an…
Session Types for Broadcasting
到目前为止，会话类型已经在点对点通信的假设下使用，以确保会话端点的线性，以及可靠的通信，以确保发送/接收二元性。在本文中，我们定义了一个会话类型论的广播通信语义，根据定义不承担点到点和可靠的通信。我们的会话框架位于广播PSI演算的参数框架之上，在参数框架内开发会话类型。我们的会话类型论具有可靠性和安全性。我们进一步相信，所提出的解决方案最终将提供一个更深入的理解会话类型的原则应如何适用于一般情况下的通信语义。
Fair Termination of Asynchronous Binary Sessions
本文提出基于线性逻辑的异步会话类型理论，利用新颖的公平异步子类型关系保证良类型进程在公平性假设下公平终止，实现无饥饿与无孤儿消息。
Session Type State Spaces Form Lattices
本研究证明良构会话类型的状态空间经强连通分量商化后构成有界格，推导得到对偶性与子类型的格理论对应关系，并在108个基准协议上完成验证，同时实现了Lean 4机械化证明。
Client-server sessions are based on a variation of the traditional interpretation of linear logic propositions as session types in which non-linear channels (those regulating the interaction between a pool of clients and a single server) are typed by coexponentials instead of the usual exponentials. Coexponentials enable the modeling of racing interactions, whereby clients compete to interact with a single server whose internal state (and thus the offered service) may change as the server processes requests sequentially. In this work we present a fair termination result for CSLL$^\infty$, a co…
Many type systems include infinite types. In session type systems, which are the focus of this paper, infinite types are important because they allow the specification of communication protocols that are unbounded in time. Usually infinite session types are introduced as simple finite-state expressions $\mathsf{rec}\, X.T$ or by non-parametric equational definitions $X\doteq T$. Alternatively, some systems of label- or value-dependent session types go beyond simple recursive types. However, leaving dependent types aside, there is a much richer world of infinite session types, ranging through v…
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…
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…
Prioritise the Best Variation
本文提出了 Priority GV (PGV)，通过解耦通道创建与线程生成并引入优先级机制，实现了对环状结构进程的无死锁类型化，并证明了其类型系统的可靠性及从 PCP 到 PGV 编码的完备性。
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈
发表机构由 AI 从论文文本抽取，如发现错误，欢迎反馈修正建议。