一句话：基于 choice trees 的 codensity 版本，通过等式推理将并发语言语义系统化地转换为编译器。
该论文关注如何从并发语言的高层语义定义出发，系统地得到编译器实现。作者以 choice trees 作为通用语义结构，并采用其 codensity 版本，使并发、非确定性等特性能够以高层代数方式表达。借助等式推理技术，论文将这类语义定义逐步变换为编译器，其中 codensity 构造是使这种计算式推导成为可能的关键。作为案例研究，论文为一个带基于通道通信的并发 lambda 演算推导出编译器，展示了该方法可处理实际并发语言特性。摘要未报告实验评估，主要通过该案例验证方法的可行性。
Choice trees have recently been introduced as a general structure for defining the semantics of programming languages with a wide variety of features and effects. In this article we focus on concurrent languages, and show how a codensity version of choice trees allows the semantics for such languages to be systematically transformed into compilers using equational reasoning techniques. The codensity construction is the key ingredient that enables a high-level, algebraic approach. As a case study, we calculate a compiler for a concurrent lambda calculus with channel-based communication.