Practical Refinement Session Type Inference (Extended Version)
Toby Ueno, Ankush Das
TL;DR
The paper tackles the annotation burden of refinement session types by introducing automatic type inference for arithmetic refinements, grounded in a sound subtyping notion via type simulation. It develops a two-stage inference algorithm that first infers base session types structurally, then resolves arithmetic refinements with Z3, and implements these ideas in Rast with three optimizations (transitivity, polynomial templates, real arithmetic) to keep inference scalable. The authors validate the approach on six challenging benchmarks, demonstrating that the optimizations are essential for practical performance and that the inferred types enable robust protocol verification. The work advances practical refinement-enabled session types, enabling safer, more expressive concurrency in real-world settings and suggesting directions for extending inference to additional Rast features.
Abstract
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.