Compiling CakeML to WASM

Picture of Michael Norrish

2 Nov 2023

The WASM (“Web Assembly”) language is an important low-level language because of its widespread availability inside the world’s deployed browsers.

CakeML is a verified functional programming language that compiles a high-level language very similar to SML into machine code across a variety of targets (e.g., x86-64, ARM and RISCV). We would like to extend that compilation so that CakeML programs can be compiled into WASM. Being formally verified means that all aspects of the compiler need to be specified in logic. In turn this means that the first stages of this project would be to port an existing formal specification of WASM into HOL4, which is the tool used to develop, specify and prove CakeML.

This project requires a student who is familiar with programming language theory, compilers, and is willing to learn how to use the HOL4 proof assistant.

You are on Aboriginal land.

The Australian National University acknowledges, celebrates and pays our respects to the Ngunnawal and Ngambri people of the Canberra region and to all First Nations Australians on whose traditional lands we meet and work, and whose cultures are among the oldest continuing cultures in human history.

arrow-left bars search times arrow-up