一句话：以 Call-by-Push-Value 为中间语言，从高阶递归函数式程序自动提取运行时间递推式，并给出指称代价语义。
程序复杂度分析常通过提取并求解反映运行时间的递推式来完成。本文提出一种从高阶递归函数式程序语法中自动提取递推式的方法：所得递推式本身是带递归的 call-by-name 语言程序，可按输入规模显式计算运行时间。为统一处理 call-by-name 与 call-by-value 两种求值策略，作者采用 Call-by-Push-Value（CBPV）作为中间语言，使提取过程不依赖具体求值顺序。最后，论文用域理论为提取出的递推式建立指称代价语义，为递推式的意义与推理提供语义基础。
The main way of analysing the complexity of a program is that of extracting and solving a recurrence that expresses its running time in terms of the size of its input. We develop a method that automatically extracts such recurrences from the syntax of higher-order recursive functional programs. The resulting recurrences, which are programs in a call-by-name language with recursion, explicitly compute the running time in terms of the size of the input. In order to achieve this in a uniform way that covers both call-by-name and call-by-value evaluation strategies, we use Call-by-Push-Value (CBPV) as an intermediate language. Finally, we use domain theory to develop a denotational cost semantics for the resulting recurrences.
@article{paperbot573,
title = {Recurrence extraction for functional programs through call-by-push-value},
author = {G. A. Kavvos and Edward Morehouse and Daniel R. Licata and Norman Danner},
journal = {Proceedings of the ACM on Programming Languages},
volume = {4},
number = {POPL},
year = {2019},
doi = {10.1145/3371083}
}