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.