Separate Compilation for a Verified Compiler

Picture of Michael  Norrish Michael Norrish

6 Feb 2023

The verified CakeML compiler compiles a functional language very similar to SML into machine code, and does so in a way guaranteed to be correct by formal proof. However, the compiler must see all of the desired program’s text all at once (it is a “whole program compiler”). To be more practical, it would be useful if the compiler could compile pieces of program text (e.g., library implementations) for later reuse by other programs. Such separately-compiled code could then be linked or dynamically loaded into other projects.

This is a PhD level project, requiring the student to develop a deep understanding of the state-of-the-art of the formal semantics of separate compilation. The student will also need to learn how to use the HOL4 theorem-proving system; existing experience with interactive theorem-provers (e.g., Coq, Lean, Isabelle) is extremely desirable.

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