Lambda the Ultimate

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.

[I hope it isn't considered out of line to post such a thing here.]

I'm launching a monthly meetup for PLT-related discussion in Berlin. We had a good get-together earlier this month, and are hoping to get some more people aboard the 10th of July. There will be talks, beverages, and at least half a dozen nerds.

See http://berlin.compilermeet.org for details.