一句话：为异常、状态、非确定性与一般递归等效应提出统一的谓词转换器语义，并导出精化关系。
对带效应的程序进行推理通常比纯程序困难得多。本文提出一种谓词转换器语义，统一处理异常、状态、非确定性和一般递归等多种效应。该语义将程序的行为刻画为从后置谓词到前置谓词的转换，并由此自然导出精化关系：一方面可将程序与其规约关联，验证程序是否满足规约；另一方面可反过来从规约出发计算（推导）出正确的带效应程序，实现“构造即正确”。文章以函数式珍珠的形式展示该语义的构造与若干应用，说明谓词转换器方法能为效应程序提供简洁、可组合的推理与开发手段。
Reasoning about programs that use effects can be much harder than reasoning about their pure counterparts. This paper presents a predicate transformer semantics for a variety of effects, including exceptions, state, non-determinism, and general recursion. The predicate transformer semantics gives rise to a refinement relation that can be used to relate a program to its specification, or even calculate effectful programs that are correct by construction.
@article{paperbot581,
title = {A predicate transformer semantics for effects (functional pearl)},
author = {Wouter Swierstra and Tim Baanen},
journal = {Proceedings of the ACM on Programming Languages},
volume = {3},
number = {ICFP},
year = {2019},
doi = {10.1145/3341707}
}