Dependent Session Types for Verified Concurrent Programming

TL;DR

This work presents TLL$_{\mathcal{C}}$, a language that merges Two-Level Linear dependent type theory with session-based concurrency to enable relational verification of concurrent programs against their sequential specs. By separating protocols from channel types and introducing dependent ghost data, it allows precise, verifiable specifications of message properties and enables proofs that concurrent implementations inherit correctness from their sequential counterparts. The authors develop a formal meta-theory, prove key properties like session fidelity and erasure safety, and implement a prototype compiler that translates TLL$_{\mathcal{C}}$ programs to safe C code, with evidence from map-reduce and mergesort demonstrations. Collectively, this framework offers a rigorous, practical path to intrinsically verified concurrent programming with robust foundations and an extensible formulation applicable beyond the current language. The work also highlights constructive approaches to recursive and multi-party session types via the protocol/channel split, paving the way for broader verification of complex distributed systems.

Abstract

We present TLLC which extends the Two-Level Linear dependent type theory (TLL) with session-based concurrency. Equipped with Martin-Löf style dependency, the session types of TLLC allow protocols to specify properties of communicated messages. When used in conjunction with the dependent type machinery already present in TLL, dependent session types facilitate a form of relational verification by relating concurrent programs with their idealized sequential counterparts. Correctness properties proven for sequential programs can be easily lifted to their corresponding concurrent implementations. TLLC makes session types a powerful tool for intrinsically verifying the correctness of data structures such as queues and concurrent algorithms such as map-reduce. To extend TLL with session types, we develop a novel formulation of intuitionistic session type which we believe to be widely applicable for integrating session types into other type systems beyond the context of TLLC. We study the meta-theory of our language, proving its soundness as both a term calculus and a process calculus. To demonstrate the practicality of TLLC, we have implemented a prototype compiler that translates TLLC programs into concurrent C code, which has been extensively evaluated.

Figures (3)

• Figure 1: Tree Diagram of Map-Reduce
• Figure 2: Spawning Tree Transformations (blue for children, red for detached sub-trees)
• Figure 3: Runtime performance comparison of variants of mergesort. SeqU = sequential mergesort with unrestricted lists; SeqL = sequential mergesort with linear lists; ConL = concurrent mergesort with linear lists; OCaml = sequential mergesort in OCaml; Rocq = sequential mergesort in Rocq.

Theorems & Definitions (201)

• theorem 1: Validity
• theorem 2: Sort Uniqueness
• theorem 3: Subject Reduction
• lemma 1: Congruence
• theorem 4: Session Fidelity
• definition 1: Reachability
• theorem 5: Global Progress
• theorem 6: Term Simulation
• theorem 7: Process Simulation
• lemma 2: Diamond Property