Practical Refinement Session Type Inference (Extended Version)

TL;DR

This paper introduces a practical type inference algorithm for session types with arithmetic refinements, reducing annotation burden and enabling safe communication protocol verification in concurrent systems.

Contribution

It presents a novel inference algorithm with optimizations, formalizes subtyping for refined session types, and demonstrates practical effectiveness with implementation and benchmarks.

Findings

Inference algorithm successfully infers session types with refinements.

Optimizations improve SMT solver performance on complex benchmarks.

Implementation in Rast shows practical applicability and efficiency.

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 $\lambda$-calculus. We show the performance benefits provided by our optimizations in coercing Z3 into solving the arithmetic constraints in reasonable time.