一句话：提出 λ-amor 类型论，用模态势类型统一高阶函数式程序的摊销代价分析，并能嵌入已有代价类型系统。
论文研究高阶函数式程序的（摊销）代价分析，旨在为已有代价类型系统提供统一理论基础。作者提出 λ-amor：一个包含表示 potential（已计入但尚未发生的代价）的模态类型的类型论框架，并结合仿射性、refinement types 与索引代价 monad 来追踪资源。作者用较简单的逻辑关系证明其可靠性。为展示表达力，论文将两个已有代价分析类型系统嵌入 λ-amor，表明它能模拟不同求值策略（call-by-name 与 call-by-value）、不同风格（effect-based 与 coeffect-based）以及有/无摊销的代价分析；其中一个嵌入还推出，对所有终止的 PCF 程序，λ-amor 具有相对完备性。
This paper presents λ-amor, a new type-theoretic framework for amortized cost analysis of higher-order functional programs and shows that existing type systems for cost analysis can be embedded in it. λ-amor introduces a new modal type for representing potentials – costs that have been accounted for, but not yet incurred, which are central to amortized analysis. Additionally, λ-amor relies on standard type-theoretic concepts like affineness, refinement types and an indexed cost monad. λ-amor is proved sound using a rather simple logical relation. We embed two existing type systems for cost analysis in λ-amor showing that, despite its simplicity, λ-amor can simulate cost analysis for different evaluation strategies (call-by-name and call-by-value), in different styles (effect-based and coeffect-based), and with or without amortization. One of the embeddings also implies that λ-amor is relatively complete for all terminating PCF programs.
@article{paperbot1202,
title = {A unifying type-theory for higher-order (amortized) cost analysis},
author = {Vineet Rajani and Marco Gaboardi and Deepak Garg and Jan Hoffmann},
journal = {Proceedings of the ACM on Programming Languages},
volume = {5},
number = {POPL},
year = {2021},
doi = {10.1145/3434308}
}