This page contains auxiliary material associated with the following submission to POPL 2014:
We refer readers to the following resources more information about our work.
The Coq formalization of Lambda-p, the core calculus presented in the paper.
- A slightly extended version of the paper (mainly with more explanations).
We expect further revisions to this paper, extending it primarily with more examples.
- The latest download of the F* compiler (version 0.7-alpha) and verifier.
This includes a mode that supports relational verification. In the zip file, all the examples relevant to our submission can
be found in the directories examples/rrf. A Makefile in that directory indicates how the examples can be verified.
- A web-facing version of the rF* verifier.