一句话：将精化组合问题对应到分离逻辑蕴涵证明，提出RCL并揭示新验证策略。
程序验证中常用精化（refinement）来证明实现满足数学规约，而整体精化通常由多个小精化组合而成。本文关注如何组合这些精化。作者发现，组合精化与在现代分离逻辑中证明蕴涵之间存在新颖对应关系：该对应一方面可复用分离逻辑的工具与抽象构造，简化组合证明；另一方面揭示了新的验证策略。为建立这一对应，论文创新性地使用天使非确定性（angelic non-determinism）应对关键挑战。基于该对应，作者提出 RCL（Refinement Composition Logic），一个专门用于组合精化的逻辑。所有结果均在 Coq 中形式化。
One successful approach to verifying programs is refinement, where one establishes that the implementation ( e.g. , in C) behaves as specified in its mathematical specification. In this approach, the end result (a whole implementation refines a whole specification) is often established via composing multiple “small” refinements. In this paper, we focus on the task of composing refinements. Our key observation is a novel correspondence between the task of composing refinements and the task of proving entailments in modern separation logic. This correspondence is useful. First, it unlocks tools and abstract constructs developed for separation logic, greatly streamlining the composition proof. Second, it uncovers a fundamentally new verification strategy. We address the key challenge in establishing the correspondence with a novel use of angelic non-determinism . Guided by the correspondence, we develop RCL (Refinement Composition Logic) , a logic dedicated to composing refinements. All our results are formalized in Coq.