程序设计语言领域顶级会议POPL’23近日公布论文录用名单，程序设计语言研究室一篇论文《Probabilistic Resource-Aware Session Types》（与美国卡内基梅隆大学合作）被该会议录用。

标题：Probabilistic Resource-Aware Session Types

作者：Ankush Das、王迪、Jan Hoffmann

摘要：

基于会话类型（Session Types）的并发编程能静态检查进程间的消息传递符合预定义的通信协议。已有的会话类型相关的工作主要关注确定性语言，但是许多消息传递系统，如马尔可夫链和随机分布式算法，是概率性的。为了实现和分析这样的系统，本文研究了概率性会话类型的元理论，并重点应用于并发系统的自动期望资源分析。概率性会话类型可以描述进程间传递的消息的概率分布，是直觉主义（二元）会话类型的一种保守扩展。为了在概率性消息通道上发送消息，进程可以使用来自概率性分支的内部随机性或者通过读取概率性消息通道来使用外部随机性。我们基于自动均摊资源分析（Automatic Amortized Resource Analysis），在本文的系统中进一步集成了期望资源上界分析。在我们的系统中，类型推导依赖于线性约束求解，并支持自动推导各种资源消耗度量的符号上界。本文的技术贡献包括基于一种新型嵌套多宇宙语义的元理论和一个类型推导算法，该算法使得程序员不用写复杂的类型注释，并支持混合使用不同的随机性来源。我们在NomosPro语言中实现了该类型系统，其类型检查算法具有线性时间复杂度。我们的实验显示NomosPro在不同领域具有应用价值，例如随机分布式算法的资源消耗分析、马尔可夫链的分析、均摊数据结构和数字合约的概率分析。NomosPro还通过以下案例展示了可伸缩性：（i）实现了两个广播协议和一个带有固定丢失概率的有界重传协议，并且（ii）验证了具有64个状态和420个转换的马尔可夫链的渐进概率分布。