一句话：提出概率精化会话类型 PReST，以符号化精化推理支持非常量概率的并发概率程序验证。
会话类型为消息传递进程间的通信协议提供形式化类型系统，近期工作虽引入概率类型构造子以分析随机化系统，但仅支持常量概率，适用性受限。本文提出概率精化会话类型，在核心演算 PReST 中实现对并发概率系统的符号推理。该类型系统是精化会话类型的保守扩展，同时支持概率选择与普通选择算子；为处理概率分支表达式的类型检查，理论在概率类型规则中对精化变量做语义量化，偏离了标准精化类型系统做法。实现采用双向类型检查器，借助 SMT 求解器重建通道的中间类型以降低标注负担。为确保证明进程几乎必然终止，作者将代价分析集成到类型系统中，得到递归深度的期望上界。评估覆盖四类基准：随机分布式协议（Itai-Rodeh 领导者选举、有界重传等）、参数化马尔可夫链（随机游走）、并发数据结构（队列）的概率分析，以及由 max、sum 等算子组合均匀分布得到的分布。实验表明类型检查器可扩展到具有复杂概率分布的大型程序。
Session types provide a formal type system to define and verify communication protocols between message-passing processes. In order to analyze randomized systems, recent works have extended session types with probabilistic type constructors. Unfortunately, all the proposed extensions only support constant probabilities which limits their applicability to real-world systems. Our work addresses this limitation by introducing probabilistic refinement session types which enable symbolic reasoning for concurrent probabilistic systems in a core calculus we call PReST. The type system is carefully designed to be a conservative extension of refinement session types and supports both probabilistic and regular choice type operators. We also implement PReST in a prototype which we use for validating probabilistic concurrent programs. The added expressive power leads to significant challenges, in both the meta theory and implementation of PReST, particularly with type checking: it requires reconstructing intermediate types for channels when type checking probabilistic branching expressions. The theory handles this by semantically quantifying refinement variables in probabilistic typing rules, a deviation from standard refinement type systems. The implementation relies on a bi-directional type checker that uses an SMT solver to reconstruct the intermediate types minimizing annotation overhead and increasing usability. To guarantee that probabilistic processes are almost-surely terminating, we integrate cost analysis into our type system to obtain expected upper bounds on recursion depth. We evaluate PReST on a wide variety of benchmarks from 4 categories: (i) randomized distributed protocols such as Itai and Rodeh’s leader election, bounded retransmission, etc., (ii) parametric Markov chains such as random walks, (iii) probabilistic analysis of concurrent data structures such as queues, and (iv) distributions obtained by composing uniform distributions using operators like max and sum. Our experiments show that the PReST type checker scales to large programs with sophisticated probabilistic distributions.