We tackle the problem of statically ensuring that message-passing programs never run into deadlocks. We focus on concurrent functional programs governed by context-free session types, which can express rich tree-like structures not expressible in standard session types. We propose a new type system based on context-free session types: it enforces both protocol conformance and deadlock freedom, also for programs implementing cyclic communication topologies with recursion and polymorphism. We show how the priority-based approach to deadlock freedom can be extended to this expressive setting. We prove that well-typed concurrent programs respect their protocols and never deadlock.

翻译：我们致力于解决静态确保消息传递程序永不陷入死锁的问题。我们重点关注受上下文无关会话类型管理的并发函数式程序，此类会话类型能够表达标准会话类型无法描述的丰富树状结构。我们提出了一种基于上下文无关会话类型的新型类型系统：该系统不仅强制协议合规性，还确保程序（包括实现递归与多态性循环通信拓扑的程序）的无死锁性。我们展示了基于优先级的无死锁方法如何扩展至这一高表达能力场景。我们证明，良类型的并发程序既遵守其协议规范，也永不发生死锁。