一句话：提出面向 context-free session types 的语法导向类型系统，并用两个 OCaml 嵌入实现检查与推断。
某些通信协议只能由 context-free session types 精确描述，它扩展传统会话类型以支持一般形式的顺序组合。然而，其复杂元理论阻碍了相应检查与推断算法的定义。本文研究一种新的、语法导向的 context-free session types 类型系统，设计上易于嵌入宿主编程语言。作者进一步给出两个 OCaml 嵌入，将 context-free session types 的检查与推断任务委托给 OCaml 类型系统，从而避免在外部实现完整推断算法。该工作为 context-free session types 提供了更实用的类型检查与推断途径。
Some interesting communication protocols can be precisely described only by context-free session types, an extension of conventional session types supporting a general form of sequential composition. The complex metatheory of context-free session types, however, hinders the definition of corresponding checking and inference algorithms. In this work, we study a new syntax-directed type system for context-free session types that is easy to embed into a host programming language. We also detail 2 OCaml embeddings that allow us to piggyback on OCaml’s type system to check and infer context-free session types.