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 twostate 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. JSVerify.fst: This is an extended version of the JSPrims library shown in our submission. As mentioned in that paper, due to space limitations, we presented a simplified version of JavaScript semantics, ignoring prototype chains, getters/setters, functionsasobjects, and other features of the language. JSVerify.fst shows our full specification, incorporating all these features. We also show an implementation of the library, verified mechanically against its specification using F*'s typechecker for the Dijkstra state monad. As mentioned in the paper, JSVerify.fst is the foundation for a verified compiler from F* to JavaScript, proven fully abstract in a POPL 2013 paper, described here.
The latest download (version 0.6alpha) 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 directoriesa Makefile in the relevant directories indicates how the examples can be verified:
Forthcoming material:
