Mechanized λJS
The Brown PLT Blog, 2012-06-04
In an earlier post, we introduced λJS, our operational semantics for JavaScript. Unlike many other operational semantics, λJS is no toy, but strives to correctly model JavaScript's messy details. To validate these claims, we test λJS with randomly generated tests and with portions of the Mozilla JavaScript test suite.
Testing is not enough. Despite our work, other researchers found a missing case in λJS. Today, we're introducing Mechanized λJS, which comes with a machine-checked proof of correctness, using the Coq proof assistant.
More work on mechanizing the actual, implemented semantics of a real language, rather than a toy.
Recent comments
9 weeks 5 days ago
14 weeks 5 hours ago
15 weeks 4 days ago
15 weeks 4 days ago
18 weeks 2 days ago
22 weeks 6 days ago
22 weeks 6 days ago
23 weeks 2 days ago
23 weeks 2 days ago
26 weeks 1 day ago