一句话：提出对时间开销敏感的操作式参数性理论，用于证明程序融合是时间改进。
参数性长期用于推理程序正确性，但现有理论对资源使用不敏感，无法刻画“一个程序比另一个使用更少资源”的程序改进。本文提出一种新的操作式参数性理论，将时间开销纳入语义，从而能够推理时间改进性质。作者通过证明若干著名程序融合技术——包括不动点融合、map 融合和 shortcut 融合——都是时间改进，展示了该理论的适用性。该工作为函数式程序的优化与资源敏感推理提供了语义基础。
Parametricity, in both operational and denotational forms, has long been a useful tool for reasoning about program correctness. However, there is as yet no comparable technique for reasoning about program improvement , that is, when one program uses fewer resources than another. Existing theories of parametricity cannot be used to address this problem as they are agnostic with regard to resource usage. This article addresses this problem by presenting a new operational theory of parametricity that is sensitive to time costs, which can be used to reason about time improvement properties. We demonstrate the applicability of our theory by showing how it can be used to prove that a number of well-known program fusion techniques are time improvements, including fixed point fusion, map fusion and short cut fusion.