一句话：提出结构余归纳的上下文形式化，为余递归程序的等式推理提供直观且相对观察等价可靠的证明方法。
结构归纳被函数式程序员和研究者广泛用于非形式推理及程序验证与语义的形式方法。本文推广其对偶——结构余归纳，用以仅依据余递归程序上下文的逻辑结构来理解它们。作者提出一种基于上下文的非形式证明方法，其风格与结构归纳证明类似，便于检查所有情况是否覆盖以及余归纳假设是否正确使用。随后，这一直观方法被形式化为一个推导程序等式的句法理论，其合理性完全依据抽象机器的计算行为建立，并相对于观察等价被证明是可靠的。
Abstract Structural induction is pervasively used by functional programmers and researchers for both informal reasoning as well as formal methods for program verification and semantics. In this paper, we promote its dual—structural coinduction—as a technique for understanding corecursive programs only in terms of the logical structure of their context. We illustrate this technique as an informal method of proofs which closely match the style of informal inductive proofs, where it is straightforward to check that all cases are covered and the coinductive hypotheses are used correctly. This intuitive idea is then formalized through a syntactic theory for deriving program equalities, which is justified purely in terms of the computational behavior of abstract machines and proved sound with respect to observational equivalence.