论文标题
液体资源类型
Liquid Resource Types
论文作者
论文摘要
本文介绍了液体资源类型，这是一种自动验证功能程序资源消耗的技术。现有的资源分析技术贸易自动化具有灵活性 - 自动化技术仅限于相对受限的资源界限家庭，而更有表现的证明技术承认价值依赖性界限取决于手写的证明。液体资源类型结合了这些方法中最好的方法，并使用逻辑改进来自动证明程序的资源消耗范围。类型系统增强了具有潜在注释的细化类型，以进行摊销资源分析。重要的是，用户可以注释数据结构声明，以指示该类型中的潜力分配是如何分配的，从而使系统可以用多项式和指数表达界限，以及根据程序值的不同表达式。我们证明了类型系统的健全性，提供了用于进行资源分析的灵活和可重复使用的数据结构的库，并使用我们的原型实现来自动验证先前需要手动证明的资源界限。
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.
