Home

Mechanized λ<sub>JS</sub>

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.

By Paul Snively at 2012-06-27 15:28 | Functional | Javascript | Lambda Calculus | Semantics | other blogs | 19310 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Thorough and

Thorough and impressive.

Important work it would be nice to see done on a more regular basis (for other languages, that is).

I just wish I could read those Coq scripts.

By Cyril at Thu, 2012-06-28 04:04 | login or register to post comments

Here's how to read them

  1. Read the datatype declarations and function definitions. Doing so is a lot like reading any other functional program.
  2. To read theorems:
    1. Start at the bottom of the dependency chain.
    2. Read each theorem statement and try to get a feel in natural language what it says. Draw pictures and instantiate it to particular cases. This is just like reading a normal mathematical theorem statement, and just like reading math, accept that this will be slow.
    3. To understand the proof, single-step through the proof script.
      1. Understand what the proof state was at each step, before running the script.
      2. Understand what the proof state was after the command modified it.
      3. Think about what mathematical argument justifies the change in the proof state.
      4. Good Coq proof scripts chain lots of tactics together.
      5. If a chain does something surprising, break it into smaller pieces and understand the intermediate states.
None of this is a fast process, but reading mathematics or code is not fast, either, and mechanized proof is a skill that builds on both of those. Also, just like in math or programming, you don't understand things until you run them, play with them, and fight with them.
By neelk at Thu, 2012-06-28 07:11 | login or register to post comments

Thank you for these

Thank you for these insights. Hopefully they'll turn out very helpful once I've given myself enough time to apply the advice on samples.

I still need to read more of the Coq documentation anyway, and understand its tactics feature, especially. Otherwise your depiction of steps totally makes sense.

Thanks again.

By Cyril at Thu, 2012-06-28 07:33 | login or register to post comments

Resources

I would add that the authors of this work rightly refer both to Benjamin Pierce et al's Software Foundations and Adam Chlipala's Certified Programming With Dependent Types for learning how to use Coq effectively. I personally have not worked through the former, but am working through the latter.

By Paul Snively at Thu, 2012-06-28 09:53 | login or register to post comments

Re: Mechanized Semantics for Mainstream Languages

Does anyone know if there is a list of mechanized (and non-mechanized) formal semantics of mainstream languages?

By George Kuan at Thu, 2012-07-05 14:36 | login or register to post comments

I haven't seen such a list.

I haven't seen such a list. It's a good idea.

By Ehud Lamm at Wed, 2012-07-25 13:37 | login or register to post comments