Theory
Prove that session-type state spaces are lattices. Develop the morphism hierarchy and connect to bisimulation.
Explore the theory →Session Types as
Algebraic Reticulates
A theory and toolchain for session types on objects, built around the insight that session-type state spaces form lattices.
17
Verified Benchmarks
8
Analysis Modules
114
Total States Analyzed
✓
All Benchmarks Are Lattices
The Reticulate Thesis
Session types describe communication protocols on objects — the legal sequences of method calls, branches, and selections. We prove that the state space of any well-formed session type, ordered by reachability, forms a lattice (which we call a reticulate).
The key insight comes from the parallel constructor
(∥), which models concurrent access to a shared object.
When two execution paths run in parallel, their combined state space is the
product lattice of the individual spaces — and products
of lattices are lattices. This makes lattice structure necessary
rather than merely nice.
Building on this foundation, we develop a morphism hierarchy (isomorphism, embedding, projection, Galois connection) between session-type state spaces, connecting to classical results in bisimulation and abstract interpretation.
Featured: Java Iterator
The java.util.Iterator protocol: repeatedly call hasNext, then next if TRUE or stop if FALSE.
rec X . hasNext . +{TRUE: next . X, FALSE: end}
4 states
4 transitions
2 SCCs
✓ Lattice
Three Pillars
Reticulate
Python library that constructs state spaces from session type definitions, checks lattice properties, and verifies protocols.
Try the tool →BICA Reborn
Java annotation-based session type checker for objects. Successor
to the original BICA (2009), with the novel ∥ constructor.
Benchmarks
17 real-world and classic protocols verified as lattices — from SMTP and OAuth to AI agent protocols (MCP, A2A).
View All Benchmarks →