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.

翻译：我们提出了TLLC，它在两级线性依赖类型理论（TLL）的基础上扩展了基于会话的并发性。借助马丁-洛夫风格的依赖关系，TLLC的会话类型允许协议指定所传递消息的属性。当与TLL中已有的依赖类型机制结合使用时，依赖会话类型通过将并发程序与其理想化的顺序对应部分关联起来，促进了一种关系验证形式。为顺序程序证明的正确性属性可以轻松地提升到其对应的并发实现上。TLLC使会话类型成为内在地验证诸如队列等数据结构和诸如Map-Reduce等并发算法正确性的强大工具。为了将会话类型扩展到TLL中，我们开发了一种新颖的直觉主义会话类型表述，我们相信这种表述可广泛应用于将会话类型集成到TLLC上下文之外的其他类型系统中。我们研究了该语言的元理论，证明了其作为项演算和进程演算的可靠性。为了展示TLLC的实用性，我们实现了一个原型编译器，可将TLLC程序翻译为并发C代码，并已进行了广泛的评估。