MSc Thesis Presentation - Lily Bryant

Name: Lily Bryant

Date: Wednesday, September 25th 2024

Time: 4 pm

Location: Zoom

Link:https://ubc.zoom.us/j/69994918392?pwd=7EWGdM4h4xc07VLR8vORsWucOt8lbe.1

Meeting ID: 699 9491 8392

Meeting Password: 083199

Supervisor's Name: William J. Bowman

Thesis Title: Compilation as Normalization: A Multi-language Semantics Approach to Compiler Correctness

Abstract:

Modern compiler projects link together diverse components, which may come from multiple source languages and be at varying stages of compilation. Compositional compiler correctness (CCC), a property which captures these intricacies, has previously required complex semantic proof theories to reason about interoperation between linked programs.

We present a purely syntactic approach for specifying and proving CCC that models compilation entirely as a reduction system. This allows us to use established techniques from term rewriting systems (TRS). To illustrate our method, we define a formal model of an A-Normal Form

(ANF) compiler using a multi-language operational semantics and show that CCC reduces to confluence, a property of rewrite systems. We also explore several common techniques for proving confluence and prove several related but weaker properties to motivate that the property should hold for the model.