On Eliminating the Impossible with Dependent Types: Choreographic Libraries with Proof-Carrying Located Values
Simon Daniel, Timon Böhler, David Richter, Pascal Weisenburger, Mira Mezini
cs.PL
Aug 20, 2026 · v1
TL;DR
ChorLean implements a dependently typed choreographic programming library in Lean, using proof-carrying located values to make endpoint projection total.
Abstract
With growing complexity, distributed software systems become increasingly challenging to maintain and reason about. When implementing a distributed protocol, developers must ensure manually that the different components fit together. Choreographic programming addresses this challenge by specifying global protocols in a single program and projecting them into communicating processes, so-called endpoints. Recent choreographic approaches are designed as programming libraries that embed this paradigm into a host language like Haskell or Rust. In these designs, we observe common cases of partiality: unreachable branches in endpoint projection (EPP) and located-value access can trigger runtime errors or undefined behavior, relying on manual discipline of library maintainers rather than being statically type-checked. Also, some programs require users to write down dummy branches that should not be reachable, for example when branching on sum types. To close this gap, we use the dependently typed Lean programming language to implement a similar choreographic library. We show how we are able to move from a partial EPP to a total EPP function, and also eliminate cases of partiality in user-written code with pattern matching on sum types. ChorLean ensures total EPP and safe value access via proof-carrying located values, passing Lean's totality checker without undefined cases, while supporting the same feature set as libraries like MultiChor.
Problem
Library-based choreographic programming embeds distributed protocol specifications in host languages, but existing libraries (in Haskell, Rust) implement endpoint projection and located-value access as partial functions with unreachable branches and runtime errors, relying on manual developer discipline rather than static checks.
Approach
ChorLean is a choreographic programming library embedded in the dependently typed Lean language. Located values carry proofs that the accessing role owns the value, making access operations total. Endpoint projection is defined as a total function accepted by Lean's totality checker, and dependent pattern matching eliminates dead branches on sum types in user code.
Results
ChorLean achieves total endpoint projection and safe value access via proof-carrying located values, passing Lean's totality checker without undefined cases, while supporting the same feature set as libraries like MultiChor.
