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.