JSCert: Certified JavaScript
Table of Contents
body
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.
Dependencies
We make use of the following Coq libraries:
- Flocq
- Flocq formalizes floating point arithmetic in Coq.
- TLC
- A non-constructive library for Coq, TLC is a general purpose Coq library that provides an alternative to Coq's standard library.
Experiments
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.