This page contains auxiliary material associated with the following paper at PLDI 2013:
This paper consolidates and extends work described in two MSR technical reports into a single conference submission.
In addition to the technical reports above, we refer readers to the following code samples and downloads for more information about our work.
prims.fst: This F* module includes the signature of the Dijkstra State Monad, a main contribution of our submission. The specific variant we use here shows a Dijkstra monad carrying a rich two-state invariant on the heap, the use of the same monad to reason about exceptions, exception handlers, and fatal errors. This is a combination of the "iDST" and "eDST" monads described in the paper.
The latest download (version 0.6-alpha) of the F* compiler and verifier, together with all our examples is available here. In the download zip file, the examples relevant to our submission can be found in the following directories---a Makefile in the relevant directories indicates how the examples can be verified: