REST: Integrating Term Rewriting with Program Verification (Artifact)

Authors Zachary Grannan , Niki Vazou , Eva Darulova , Alexander J. Summers

Thumbnail PDF

Artifact Description

  • Filesize: 0.49 MB
  • 2 pages

Document Identifiers

Author Details

Zachary Grannan
  • University of British Columbia, Vancouver, Canada
Niki Vazou
  • IMDEA Software Institute, Madrid, Spain
Eva Darulova
  • Uppsala University, Sweden
Alexander J. Summers
  • University of British Columbia, Vancouver, Canada


We thank Jonathan Chan, Eric Conlon, Rui Ge, Paulette Koronkevich and the anonymous reviewers for their helpful and constructive feedback.

Cite AsGet BibTex

Zachary Grannan, Niki Vazou, Eva Darulova, and Alexander J. Summers. REST: Integrating Term Rewriting with Program Verification (Artifact). In Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 2, pp. 12:1-12:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Artifact Evaluation Policy

The artifact has been evaluated as described in the ECOOP 2022 Call for Artifacts and the ACM Artifact Review and Badging Policy


This artifact contains code for REST, a novel term rewriting technique for theorem proving that uses online termination checking and can be integrated with existing program verifiers. The artifact includes the REST library as well as a version of Liquid Haskell extended with REST. In addition, it includes the scripts that were used to generate the tables in the paper’s evaluation section. Also included is a docker image containing a development environment for REST (and the Liquid Haskell extension).

Subject Classification

ACM Subject Classification
  • Theory of computation → Program verification
  • term rewriting
  • program verification
  • theorem proving


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail