论文标题
休息：将术语重写与程序验证（扩展版本）集成
REST: Integrating Term Rewriting with Program Verification (Extended Version)
论文作者
论文摘要
我们介绍了REST，这是一种用于定理的新型术语重写技术，证明使用在线终止检查，可以与现有程序验证符集成。 REST可以为定理的灵活但终止术语重写：（1）利用比标准重写简化订单更允许的新引入的定期订单； （2）基于到目前为止的重写路径动态和迭代选择订单； （3）集成外部牙齿，允许使用重写规则的步骤。我们的休息方法是围绕易于实现的核心算法设计的，可以通过定期顺序及其实现的选择参数化；这样，我们的方法就可以轻松地集成到现有工具中。我们将REST作为Haskell库实施，并将其纳入Liquid Haskell的评估策略，从而扩展了Liquid Haskell的重写规则。我们通过将其与现有重写技术和电子匹配的现有重写技术进行比较，并证明它可用于在许多现有的液体Haskell证明中取代手动引理应用程序，从而评估了我们的休息实现。
We introduce REST, a novel term rewriting technique for theorem proving that uses online termination checking and can be integrated with existing program verifiers. REST enables flexible but terminating term rewriting for theorem proving by: (1) exploiting newly-introduced term orderings that are more permissive than standard rewrite simplification orderings; (2) dynamically and iteratively selecting orderings based on the path of rewrites taken so far; and (3) integrating external oracles that allow steps that cannot be justified with rewrite rules. Our REST approach is designed around an easily implementable core algorithm, parameterizable by choices of term orderings and their implementations; in this way our approach can be easily integrated into existing tools. We implemented REST as a Haskell library and incorporated it into Liquid Haskell's evaluation strategy, extending Liquid Haskell with rewriting rules. We evaluated our REST implementation by comparing it against both existing rewriting techniques and E-matching and by showing that it can be used to supplant manual lemma application in many existing Liquid Haskell proofs.
