This page contains auxiliary material associated with the following submission to PLDI 2013:

We refer readers to the following resources more information about our work.

  • 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.6-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.
  • The Coq formalization of Lambda-p, the core calculus presented in the paper.

    • Forthcoming material:

    • A web-facing version of the rF* verifier.