back to paper page
# Recalling a Witness

## Software artifacts (evaluated by the POPL AEC)

#### Section 2 of the paper

#### Section 3 of the paper

#### Section 4 of the paper

The examples and case studies described in Sections 2, 3, and 4 of this paper 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.

The AEC evaluated these examples and case studies as they were presented in F⭑ release v0.9.5.0. These artifacts were subsequently polished further to better match the text in the final version of the paper, see this commit in the master branch of the F⭑ repository. However, as F⭑ is a language that is actively developed, the contents of the files listed below might have changed since this paper was published.

The examples and the supporting library code are in the
following files in the F⭑ master branch

(as of this
commit;
the given filepaths are relative to the
top-level `fstar` directory):

`ulib/FStar.Monotonic.Heap.fsti`- Basic heap model interface with support for monotonic references

`ulib/FStar.Monotonic.Heap.fst`- Implementation of the basic heap model interface

`ulib/FStar.Heap.fst`- Plain heap model where all the references have trivial preorder

`ulib/FStar.ST.fst`- Implementation of the STATE effect using the heap model

`ulib/FStar.MRef.fst`- Utility functions for monotonic references

`examples/preorders/SnapshotST.fst`- An example of temporarily escaping the preorder

`ulib/FStar.Monotonic.HyperHeap.fst`- Region-based hyperheap model with support for monotonic references

`ulib/FStar.Monotonic.HyperStack.fst`- Region-based hyperstack model with support for monotonic references

`ulib/FStar.Monotonic.RRef.fst`- Utility functions for hyperstack monotonic references

`examples/preorders/MonotonicArray.fst`- The monotonic array library

`examples/preorders/Protocol.fst`- The file transfer case study

`examples/preorders/Ariadne.fst`- The Ariadne protocol case study