一句话：提出 Liquid 资源类型，用精化类型与潜势标注自动验证函数式程序的精确资源消耗界。
资源分析长期在自动化与表达力之间取舍：自动方法只能处理受限的资源界，依赖值的精确界往往需要手写证明。本文提出 Liquid 资源类型，将逻辑精化与潜势（potential）标注结合，借助精化类型对函数式程序进行摊销资源分析。其关键点是允许用户在数据结构声明上标注潜势在类型内的分配方式，从而表达多项式、指数以及依赖程序值的更精确资源界。作者证明了该类型系统的可靠性，并提供了可复用、灵活的数据结构库，用于开展资源分析。原型实现能够自动验证此前需要人工证明的资源界，展示了该方法在保持自动化的同时提升表达力的效果。
This article presents liquid resource types, a technique for automatically verifying the resource consumption of functional programs. Existing resource analysis techniques trade automation for flexibility – automated techniques are restricted to relatively constrained families of resource bounds, while more expressive proof techniques admitting value-dependent bounds rely on handwritten proofs. Liquid resource types combine the best of these approaches, using logical refinements to automatically prove precise bounds on a program’s resource consumption. The type system augments refinement types with potential annotations to conduct an amortized resource analysis. Importantly, users can annotate data structure declarations to indicate how potential is allocated within the type, allowing the system to express bounds with polynomials and exponentials, as well as more precise expressions depending on program values. We prove the soundness of the type system, provide a library of flexible and reusable data structures for conducting resource analysis, and use our prototype implementation to automatically verify resource bounds that previously required a manual proof.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2006-16233,
title = {Liquid resource types},
author = {Tristan Knoth and Di Wang and Adam Reynolds and Jan Hoffmann and Nadia Polikarpova},
journal = {Proceedings of the ACM on Programming Languages},
volume = {4},
number = {ICFP},
year = {2020},
doi = {10.1145/3408988}
}