Skip to content

Home

Jump to bottom Edit New page
sidprasad edited this page Jul 31, 2014 · 8 revisions

Rewrite Verification System Wiki

Welcome to the Rewrite Verification System Wiki. This wiki provides documentation for:

  • checkpc : A certified equality verification system. checkpc can help reduce the number of correctness checks in systems that involve rewriting, without sacrificing the validity of the results produced. Given the importance of rewriting and equational reasoning in automated deduction, symbolic algebra, programming languages, etc. it can help reduce redundancy and ensure correctness of several systems.

  • rwthree: This is a naive rewriting and equality checking system that demonstrates the use of the checkpc verifier. Individual rewrites produced by the system are verifiable by checkpc

A technical report for checkpc is available here.

Code is available here.

Add a custom footer
Add a custom sidebar
Clone this wiki locally