hide
Free keywords:
Computer Science, Programming Languages, cs.PL
Abstract:
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.
