一句话：提出一种基于 sized 类型推断、ticking 单子变换与约束求解的全自动高阶函数式程序复杂度分析方法。
针对高阶函数式程序的复杂度分析，本文提出一套可全自动化的方法。其核心由三部分组成：用于尺寸分析且可靠的类型系统、该类型系统的可靠类型推断过程，以及 ticking 单子变换与约束求解。方法通过抽象索引语言和高阶索引多态等机制，提升推断能力与适用范围。作者给出了原型实现，并在若干示例上验证：该工具能够分析多数竞争方法无法处理的程序，表明基于 sized 类型的自动化复杂度分析可行。
This paper introduces a new methodology for the complexity analysis of higher-order functional programs, which is based on three ingredients: a powerful type system for size analysis and a sound type inference procedure for it, a ticking monadic transformation and constraint solving. Noticeably, the presented methodology can be fully automated, and is able to analyse a series of examples which cannot be handled by most competitor methodologies. This is possible due to various key ingredients, and in particular an abstract index language and index polymorphism at higher ranks. A prototype implementation is available.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{AvanziniL17,
title = {Automating sized-type inference for complexity analysis},
author = {Martin Avanzini and Ugo Dal Lago},
journal = {Proceedings of the ACM on Programming Languages},
volume = {1},
number = {ICFP},
year = {2017},
doi = {10.1145/3110287}
}