A Compositionally Verified Compiler for a Higher-Order Imperative Language [pdf] (mpi-sws.org) 18 points by gkuan 11y ago ↗ HN
[–] kungfooman 11y ago ↗ Too theoretical, needs something practical in browser to live test. [–] Retra 11y ago ↗ So make it. You've got the theory right there. [–] cyrus_ 11y ago ↗ I don't know about running them in a browser, but the related projects CakeML [1] and CompCert [2] are both pretty easy to download and run, and very featureful.[1] https://cakeml.org/ [2] http://compcert.inria.fr/compcert-C.html
[–] cyrus_ 11y ago ↗ I don't know about running them in a browser, but the related projects CakeML [1] and CompCert [2] are both pretty easy to download and run, and very featureful.[1] https://cakeml.org/ [2] http://compcert.inria.fr/compcert-C.html
3 comments
[ 3.4 ms ] story [ 22.5 ms ] thread[1] https://cakeml.org/ [2] http://compcert.inria.fr/compcert-C.html