SHF:Small: Enriching Session Types for Practical Concurrent Programming

由于许多应用程序的分布式特性和性能提升的前景，并发编程正变得越来越普遍。然而，由于数据竞争和死锁的存在，并发编程也是出了名的容易出错。并发编程的一种很有前途的方法是消息传递并发，这是因为它具有更高级别的抽象。消息传递并发性已被各种实用编程语言采用，如Erlang、Go和Rust。例如，Serve是在Rust中开发的一个实验性浏览器引擎，它利用任务的消息传递并发性，如DOM遍历、布局绘制和JavaScript执行。该研究项目研究了会话类型在实际消息传递并发中的应用，同时解决了数据竞争和死锁的陷阱。会话类型允许对消息交换协议进行表达式和编译时检查。该项目的智力优势是提升了会话类型的表现力，以适应当今的并发通信模式，同时保持其逻辑基础的真实性。这个研究项目的逻辑基础是最近发现的直觉线性逻辑和会话类型之间的Curry-Howard同构，它将线性命题与会话类型联系起来，将顺序演算证明与并发进程联系起来，并将简约化为消息传递通信。建立在此基础上的现有工作提供了强有力的保证，但也缩小了会话类型的适用性。这项研究的目的有两个：(I)增加会话类型的适用性，同时保持其逻辑基础不变，以及(Ii)展示所产生的技术对现实世界软件开发的实用性。对于(Ii)，该项目探索了(I)产生的技术在伺服代码库中的应用。对于(I)，该项目首先探索引入共享频道，以支持根据情况性质或出于性能考虑而需要共享的程序。这种探索中的关键问题是防止共享通道上的数据竞争，以保证会话保真度和保证某种形式的全球进展。在最简单的形式下，全球进步将缺乏僵局自由，这是一种纯粹线性环境下的属性。在第二阶段，给出了死锁预防的逻辑解释。在第三阶段，该项目探索了使用依赖类型来丰富会话类型，以表达和验证主要与协议无关的属性。在所有情况下，都给出了可靠性的证明以及适应所开发技术的会话型并发编程语言的原型。

Concurrent programming is becoming increasingly prevalent because of the distributed nature of many applications and the prospect of performance gains. However, concurrent programming is also notoriously error-prone because of the presence of data races and deadlocks. A promising approach to concurrent programing is message-passing concurrency, due to its higher-level of abstraction. Message-passing concurrency has been adopted by various practical programming languages, such as Erlang, Go, and Rust. Servo, for example, is an experimental browser engine developed in Rust that exploits message-passing concurrency for tasks, such as DOM traversal, layout painting, and JavaScript execution. This research project studies the application of session types to practical message-passing concurrency, while addressing the pitfalls of data races and deadlocks. Session types allow the expression and compile-time checking of the protocols of message exchange. The project's intellectual merits are to lift the expressiveness of session types to accommodate today's concurrent communication patterns, while remaining truthful to their logical foundation. The project's broader significance and importance are its provision of both a foundational and practical view on concurrent programming, the development of curricular material at the sophomore-level, and a session type extension for Rust.The logical foundation of this research project is the recently discovered Curry-Howard isomorphism between intuitionistic linear logic and session types, which relates linear propositions to session types, sequent calculus proofs to concurrent processes, and cut reduction to message-passing communication. Existing work building on this foundation provides strong guarantees, but also narrows the applicability of session types. The aim of this research is two-fold: (i) to increase the applicability of session types, while keeping their logical foundation intact, and (ii) to demonstrate practicality of the resulting techniques to real-world software development. For (ii), the project explores the application of the techniques resulting from (i) to the Servo code base. For (i), the project first explores the introduction of shared channels to support programs that demand sharing by the nature of circumstances or for performance considerations. Key concerns in this exploration are the prevention of data races along shared channels to guarantee session fidelity and the assurance of a form of global progress. In its simplest form, global progress will lack deadlock freedom, a property holding in the purely linear setting. In a second phase, a logical interpretation of deadlock prevention is derived. In a third phase, the project explores the enrichment of session types with dependent typing for the expression and verification of properties that are not primarily protocol-related. In all cases, proofs of soundness as well as a prototype of a session-typed concurrent programming language accommodating the developed techniques are given.