Auxiliary materials for Dijkstra Monads for Free
back to paper page

Dijkstra Monads for Free

Software artifacts (evaluated by the POPL AEC)

Implementation in F⭑

The techniques described in this paper (e.g. in Subsections 3.5 and 4.6) have been implemented in F⭑ (master branch). F⭑ is open source software, it is available on Github, and it is known to work well on Windows, Mac, and Linux. Instructions for building from source are available at INSTALL.md.

As a backup plan we have also prepared a Linux VM with everything that is needed to build F⭑ from source and with a working binary, everything as of October 2016 at the time of the artifact evaluation. It can be downloaded as an OVA archive, or just the disk image in VMDK format (xzipped). The user name is 'edsger' and the password is 'monad'. To use this VM you currently need to open a terminal and type:

$ cd ~/FStar/examples/dm4free
$ make

After this you can try out the various examples below by running fstar.exe NameOfExample.fst. The VM has the emacs and vim editors installed with F⭑-specific modes installed. In case you wish to update F⭑ to the very latest GitHub version you can optionally do this:

$ cd ~/FStar
$ git pull
$ make -C src ocaml-fstar-ocaml
Some notes on the implementation of Dijkstra monads for free in F⭑ are available at various places.

Examples in F⭑

The examples from Section 2 are also available in the F⭑ repo and work as expected. Here is in which file each of the example lives:

back to paper page