Auxiliary materials for Recalling a Witness
back to paper page

Recalling a Witness

Software artifacts (evaluated by the POPL AEC)

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

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):

Section 2 of the paper

Section 3 of the paper

Section 4 of the paper

back to paper page