No description, website, or topics provided.
Coq Other
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
detritus
.gitignore
Heap.v
Makefile
PersistentArrays.v
README.md
Refinement.v
Sqrt.v
Swap.v
While.v

README.md

dtp-refinement

The Coq library supporting the paper "Embedding the Refinement Calculus in Coq".

The Coq scripts are organized as follows:

Script Description
Heap.v Model of the heap.
Refinement.v Encoding of Predicate Transformers.
While.v While language; refinement lemmas, and tactics.
Swap.v Swap example.
Sqrt.v Square root example.
PersistentArrays.v Persistent Arrays case-study.

Run make to compile all.