JSkel : A JavaScript semantics in Skeletal

JSkel is a skeletal project born in the Celtique at Inria Rennes in September 2019 and it's the first real-world language implementation in Skeletal Semantics http://skeletons.inria.fr/.

The idea behind this project is to exploit as much as possible, necro, the tool for writing in skel, the language equivalent the skeletal semantics. Goal of this project is to have the best representation possible of JavaScript semantics going halfway between a rigorous formal approach and a more practical one.

This project may look very practical, but formalism are hidden under the hood thanks to what necro allows.

Principles of these experience are appliable to most of the multi-paradigm languages.

This is a work in progress work in which we try to keep track of all the functional versions. The first one got lost, but we were able to evaluate expressions.

If the semantics of the language is represented in skel, the syntactical part relies on the Flow Parser. This parser is a JavaScript parser written in OCaml. It produces an AST that conforms to SpiderMonkey's Parser API and that mostly matches what esprima produces. The Flow Parser can be compiled to native code or can be compiled to JavaScript using js_of_ocaml.

The project consists of:

• A Semantics of JS, indeed src/js.sk
• An instantiation of the interpreter in the folder ./parser

Dependencies

• OCaml (4.09 or greater)
• necro
• Flow parser (https://github.com/facebook/flow/tree/master/src/parser)
• ocaml-migrate-parsetree.1.8.0

Parser

opam install ocaml-migrate-parsetree.1.8.0
opam pin add flow_parser https://github.com/facebook/flow.git
opam install flow_parser

remember to not update ocaml-migrate-parsetree

Runnig example

At the actual state an example of the running semantics is given in the parse folder. See Readme in the ./parser folder