Code is available on our github page. We describe our development on this page.
Alternatively, you may download the Open Virtualization Format VM here. Warning: that file is over 1.2G.
We make use of the following Coq libraries:
- Flocq formalizes floating point arithmetic in Coq.
- A non-constructive library for Coq, TLC is a general purpose Coq library that provides an alternative to Coq's standard library.
In the course of this work, we have discovered some interesting browser behaviours. You can read about various major browser interpretations of try-catch-finally here.