This page contains auxiliary material associated with our work on compiling F* to JavaScript, described in this POPL 2013 paper.

We frequently update this page to record the current status of our tools and to provide more details about our theory.

A primer on full abstraction and an interactive tutorial, including a game to test our full-abstraction result in practice--let us know if you win the game!

An informal presentation and a web-based demo of a prototype ML compiler bootstrapped in JavaScript (much recommended for a quick review of the fully abstract compilation work). This includes a demo of running a tiny ML to JavaScript compiler within your browser as JavaScript.

JSExec.fs: This is an F# module containing an executable specification of our JavaScript runtime.

ex.fst and ex.fst.js: An example F* source module (in fact a simplified version of prims.fst) and the output of our fully abstract compiler to JavaScript on this file. Our implementation includes a number of practical features in addition to the formal compiler in the paper. This includes support for modules with private fields and abstract types, importing trusted values from the context (e.g., DOM functions) for use within F*, support for exporting values at polymorphic types with runtime type representations, etc.

An updated version of the F* metatheory in Coq, including the handling of exceptions, fatal error, and direct-style state.

An updated source release of the F* compiler, including the JavaScript verification and compilation tools.

Forthcoming material:

  • An updated web-facing version of our compiler, with JS tools