The Coq source code can be downloaded here.
fletch_main.v contains the message safety theorem and proof.
The implementation of message-safe and strict type checkers can be downloaded here.
In order to be able to run our experiments, please follow the steps below:
gclientis on your path environment variable
gclient sync --revision 45011 -n && gclient runhooks
./main.sh compile, otherwise follow the instructions here
(pathToFolder)is the path to the
ReleaseX64/might change depending on your operating system version
./main.shto run the experiments (see
README.txtfor more details about the experiments)
pub cache repair
When you run the experiments typing
./main.sh, a graphical interface will appear, and after the experiment execution a pdf file
will be generated and displayed.
If you have trouble running the experiments, or some tool such as latex is not installed on your machine, you can type
./benchmarks.sh (name), where
(name) is the benchmark name (for example dart2js).
This command will prompt the experiment result as plain text.
If you set the environment variable as mentioned above, you can run the type checker on a single file
file.dart with the standard Dart
type checker by typing
If you want to use the message-safety type checker you can run
dartanalyzer --message-safe file.dart,
and to run the full type safety checker type
dartanalyzer --message-safe --strict file.dart