Session types express and enforce safe communication in concurrent message-passing systems by statically capturing the interaction protocols between processes in the type. Recent works extend session types with arithmetic refinements, which enable additional fine-grained description of communication, but impose additional annotation burden on the programmer. To alleviate this burden, we propose a type inference algorithm for a session type system with arithmetic refinements. We develop a theory of subtyping for session types, including an algorithm which we prove sound with respect to a semantic definition based on type simulation. We also provide a formal inference algorithm that generates type and arithmetic constraints, which are then solved using the Z3 SMT solver. The algorithm has been implemented on top of the Rast language, and includes 3 key optimizations that make inference feasible and practical. We evaluate the efficacy of our inference engine by evaluating it on 6 challenging benchmarks, ranging from unary and binary natural numbers to linear $λ$-calculus. We show the performance benefits provided by our optimizations in coercing Z3 into solving the arithmetic constraints in reasonable time.

翻译：会话类型通过在类型中静态捕获进程间的交互协议，表达并强制并发消息传递系统中的安全通信。近期研究将算术精化扩展至会话类型，使得通信能够进行更细粒度的描述，但同时也给程序员带来了额外的标注负担。为减轻此负担，我们提出了一种支持算术精化的会话类型系统的类型推断算法。我们发展了会话类型的子类型理论，包括一种算法，并证明了该算法相对于基于类型模拟的语义定义是可靠的。我们还提供了一种形式化的推断算法，该算法生成类型与算术约束，随后通过Z3 SMT求解器进行求解。该算法已在Rast语言基础上实现，并包含3项关键优化，使得推断变得可行且实用。我们通过在6个具有挑战性的基准测试（从一元和二元自然数到线性$λ$-演算）上评估我们的推断引擎，验证了其有效性。我们展示了所提出的优化在促使Z3在合理时间内求解算术约束方面带来的性能优势。