Session type state spaces form lattices with useful properties
Session Type State Spaces Form Lattices
Programming LanguagesLogic in Computer Science
Summary
The authors found that the possible states of communication protocols, called session types, can be organized into a mathematical structure known as a bounded lattice. This structure helps understand how protocols combine and relate to each other. They tested their discovery on many real-world protocols from fields like networking and AI, confirming the pattern. Their findings also clarify how certain operations preserve these structures and relate to protocol subtyping.
What this means in practice
- •For protocol developers: Design and verify communication protocols by leveraging the lattice structure of their session types for better compositional reasoning.
- •For distributed systems engineers: Use the lattice-based framework to analyze and optimize interactions in distributed protocols ensuring correctness under composition.
Authors
Alexandre Zua Caldeira
Abstract
We prove that the state space of every well-formed session type, quotiented by strongly connected components, forms a bounded lattice; n-ary parallel composition yields product lattices. Two consequences follow: duality preserves the lattice up to isomorphism, and Gay-Hole width subtyping corresponds to lattice embedding for non-recursive types. We validate this on 108 benchmark protocols across networking, databases, distributed systems, AI, and fault tolerance: all form lattices, 93 distributive, 15 non-distributive. Mechanised in Lean 4 with two independently developed tool implementations.