This project was written for my University of Cambridge BA Computer Science Part II dissertation.
l1c is a verified compiler for the L1 language presented in the Cambridge Semantics of Programming Languages course.
The target language is a slight modification of the vsm0 VM presented in the Cambridge Compiler Construction course.
The operational semantics of these two languages can be found in:
The compiler is verified, meaning that there exists a proof that the compiler preserves the semantics of a program. The main correctness result can be found here.
The produced dissertation can be found in the dissertation directory. This repository is made available for illustration purposes; if you have a comprehension issue, feel free to file an issue.
Many thanks to Ramana Kumar and Magnus Myreen, who gave me important feedback over the course of the project.