Papers With

← All papers
First page of Session Type State Spaces Form Lattices

Session Type State Spaces Form Lattices

Alexandre Zua Caldeira

cs.PL Sep 28, 2026 · v1 cs.LO
formalization verification logic
Read PDF arXiv abstract
TL;DR
Formalizes in Lean 4 that well-formed session type state spaces form bounded lattices, with duality and subtyping consequences.
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.
Problem

Session types describe communication protocols, but their structural properties as ordered state spaces were not rigorously characterized. It was unclear whether session type state spaces form lattices and how duality and subtyping relate to lattice structure.

Approach

The state space of each well-formed session type, quotiented by strongly connected components, is proven to form a bounded lattice, with n-ary parallel composition yielding product lattices. Duality is shown to preserve the lattice up to isomorphism, and Gay-Hole width subtyping is shown to correspond to lattice embedding for non-recursive types. The results are mechanised in Lean 4 with two independently developed tool implementations.

Results

All 108 benchmark protocols across networking, databases, distributed systems, AI, and fault tolerance form lattices; 93 are distributive and 15 non-distributive.