Dependent Session Types for Verified Concurrent Programming

TL;DR

This paper introduces TLLC, an extension of a dependent type theory with session-based concurrency, enabling verified concurrent programming through relational verification and practical implementation.

Contribution

It develops a novel formulation of intuitionistic session types and integrates them into TLL, with formal meta-theory and a prototype compiler for verified concurrent C programs.

Findings

Proven soundness of TLLC as a term and process calculus

Successful implementation of a compiler translating TLLC to C

Demonstrated verification of concurrent data structures and algorithms

Abstract

We present TLLC which extends the Two-Level Linear dependent type theory (TLL) with session-based concurrency. Equipped with Martin-L\"{o}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.