In English

A Compiler from CakeML to JavaScript

Oskar Nyberg
Göteborg : Chalmers tekniska högskola, 2018. 62 s.
[Examensarbete på avancerad nivå]

This thesis presents a new compiler from CakeML to JavaScript with support for almost the entire CakeML language. In addition to the new compiler, a JavaScript syntax formalization has been defined together with formal semantics for a subset of JavaScript. The semantics include coverage for language features introduced as part of the ECMAScript 2015 standard. The new compiler, syntax formalization and semantics are implemented in the HOL4 theorem prover to allow for future verification of the new compiler.

The new compiler enables CakeML programs to be run in web browsers on both desktop computers and smart phones and other contexts previously not available to CakeML.

Nyckelord: Compiler, Transpiler, Formal, Semantics, Verification, CakeML, JavaScript, ECMAScript

Publikationen registrerades 2018-08-16. Den ändrades senast 2018-08-16

CPL ID: 255702

Detta är en tjänst från Chalmers bibliotek