SCS Undergraduate Thesis Topics
|Matt McKay||Karl Crary||Compiler Correctness via Contextual Equivalence|
We have developed a methodology for verifying the correctness of the closure conversion phase of a compiler, adapted from the work by Ahmed. This lets us verify that individual components of programs are compiled correctly, so they can be linked with any other code and still behave as desired. We do this by using a shared language that encompasses both the source and target languages in which the compiled code can be reasoned about alongside its source. Our main improvement over previous methods is that we donbarticulators to construct a voice for BF.t need boundaries that separate the source and target language while inside the shared language.