一句话：提出参数化单子翻译，统一刻画高阶计算中的终止性、连续性与复杂性。
该论文针对高阶计算中终止性、连续性与复杂性等概念通常分散处理的问题，为一系列按值调用（call-by-value）函数式语言建立参数化单子翻译，并证明其可靠性定理。作者给出多种具体实例，表明这些基本概念都可纳入同一框架。作为副产品，还得到：（i）从 System T 及其扩展中可定义的闭泛函 (N→N)→N 提取连续性模的方法；（ii）对 bar recursion 时间复杂性的刻画。整体目标是为高阶计算提供统一语义框架。
We set up a parametrised monadic translation for a class of call-by-value functional languages, and prove a corresponding soundness theorem. We then present a series of concrete instantiations of our translation, demonstrating that a number of fundamental notions concerning higher-order computation, including termination, continuity and complexity, can all be subsumed into our framework. Our main goal is to provide a unifying scheme which brings together several concepts which are often treated separately in the literature. However, as a by-product, we also obtain (i) a method for extracting moduli of continuity for closed functionals of type $(\mathbb{N}\to\mathbb{N})\to\mathbb{N}$ definable in (extensions of) System T, and (ii) a characterisation of the time complexity of bar recursion.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{Powell20,
title = {A unifying framework for continuity and complexity in higher types},
author = {Thomas Powell},
journal = {Logical Methods in Computer Science},
volume = {Volume 16, Issue 3},
year = {2020},
doi = {10.23638/lmcs-16(3:17)2020}
}