Practical Refinement Session Type Inference (Extended Version)
Toby Ueno, Ankush Das

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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Formal Methods in Verification · Security and Verification in Computing
