Featherweight JavaScript?

I am looking for a calculus representing the core features of JavaScript (ECMAScript), in the same way as Featherweight Java calculus does that for Java.
Unfortunately, the only calculus I was able to find is JS0T described in Towards Type Inference for JavaScript.
A quick glance made me suspicious to the faithfulness of JS0T in respect to JavaScript, as for example, objects are typed as recursive records. While this is a common approach in OO calculi, I believe using it for JavaScript is unjustified - to my knowledge, "this" is defined dynamically, not lexically, so to speak.

Could anyone please point me to the right direction (either by providing references, or by negating my suspicion)?

Thanks a lot!

Comment viewing options

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

slim pickings

There's not very much theoretical work on JavaScript. One of the difficulties is that it's a hybrid language, so what makes a core calculus "core" depends on what aspects you want to study. It's functional, so the lambda calculus would be faithful to one aspect of the language, and it's object-oriented, so an Abadi-Cardelli-style calculus would also work. If you're interested in types like FJ was, well, unless you're discussing the addition of static types to JS (as in the link you provided), there's not much point for ES3.

Another difficulty is that the semantics is highly imperative, which I think would make it even more difficult to do the kind of semantic hacks the FJ folks did to simulate the semantics of an imperative language without introducing mutation into the model. For exmaple, object construction works by handing a procedure a vanilla object and allowing it to create and mutate arbitrary fields.

Cormac Flanagan and I (but more Cormac) have gone through a number of little calculi in discussing various aspects of the design of ES4, mostly from the perspective of studying the ES4 type system. At some point those might show up in papers, but we don't have any immediate plans for that.

Scoping

Hi Dave, I already checked ES Wiki before asking, but spotting your name came back to LtU :)

My current concern with JS (or ES for that matter) is scoping, including "this". I found it very difficult to explain to people how JS scoping works, and how objects differ from other namespaces, so I hoped a little calculus would help. I believe the calculus could even drop I/O, and prototypes, and constructors, and "eval", as long as assignment, and closures, and "this" are covered (and optionally "with" and other methods for converting between different namespaces).

Well, will add this to my list of "nice to do" projects.

well...

You could always look at my half-baked, unfinished, buggy, ASCII notes sketching an operational semantics for a core of JS similar to what you're talking about ("ClassicJavaScript"). But don't trust it. :)

JS Semantics

JavaScript instrumentation for browser security gives a semantics for JavaScript, though it's most likely not what you're looking for. They care more about the JavaScript setting than the language itself, and don't really treat the language features in detail. You might find something you like in their JS-related references.

semantics of the DOM

That's more like a semantics for the DOM, rather than the language itself. Which is a very interesting problem in and of itself, but it's explicitly excluded from the ECMAScript spec and as you say probably not what Andris was looking for.