一句话：展示如何用 Liquid Haskell 的 refinement types 在同一框架中验证程序效率与资源使用。
本文探讨如何在 Liquid Haskell 中不仅推理程序正确性，还能推理程序效率。Liquid Haskell 通过将逻辑性质编码为 refinement types 来支持形式化推理。作者复用其现有验证机制，使代价分析结果得到验证，并针对特定程序上下文引入自定义不变量以保证分析精度。为说明该方法，他们对多种常用数据结构和算法进行了效率分析，并探索了不同资源使用概念。经验表明，在 Liquid Haskell 中推理效率通常与推理正确性一样简单，且两者可以自然结合。
Liquid Haskell is an extension to the type system of Haskell that supports formal reasoning about program correctness by encoding logical properties as refinement types. In this article, we show how Liquid Haskell can also be used to reason about program efficiency in the same setting. We use the system's existing verification machinery to ensure that the results of our cost analysis are valid, together with custom invariants for particular program contexts to ensure that the results of our analysis are precise. To illustrate our approach, we analyse the efficiency of a wide range of popular data structures and algorithms, and in doing so, explore various notions of resource usage. Our experience is that reasoning about efficiency in Liquid Haskell is often just as simple as reasoning about correctness, and that the two can naturally be combined.
@article{paperbot568,
title = {Liquidate your assets: reasoning about resource usage in liquid Haskell},
author = {Martin A. T. Handley and Niki Vazou and Graham Hutton},
journal = {Proceedings of the ACM on Programming Languages},
volume = {4},
number = {POPL},
year = {2019},
doi = {10.1145/3371092}
}