流动资源类型
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
