Open Collections

Bryant, Lily

University of British Columbia

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.

Text

2024-08-29

Attribution-NonCommercial-NoDerivatives 4.0 International

http://hdl.handle.net/2429/89101

Computer Science

University of British Columbia

UBCV

http://creativecommons.org/licenses/by-nc-nd/4.0/