一句话：将编译器正确性推导从仅收敛行为扩展到同时处理发散行为，用部分性单子显式表示发散并支持等式式计算。
已有工作提出从正确性规约直接计算正确编译器的方法，但只考虑源语言的收敛行为，因而对发散程序可能生成任意错误代码。本文将该方法自然扩展为同时处理收敛与发散行为，无需分别推理。核心是用部分性单子（partiality monad）把发散显式化，并用强互模拟（strong bisimilarity）支持等式式推导。这样便可在统一框架中从规约计算编译器，且通过替换底层单子可推广到其他效应。论文以函数式珍珠形式展示该方法，说明其能避免为发散单独推理，并保持计算式推导风格。
Bahr and Hutton recently developed a new approach to calculating correct compilers directly from specifications of their correctness. However, the methodology only considers converging behaviour of the source language, which means that the compiler could potentially produce arbitrary, erroneous code for source programs that diverge. In this article, we show how the methodology can naturally be extended to support the calculation of compilers that address both convergent and divergent behaviour simultaneously , without the need for separate reasoning for each aspect. Our approach is based on the use of the partiality monad to make divergence explicit, together with the use of strong bisimilarity to support equational-style calculations, but also generalises to other forms of effect by changing the underlying monad.