LFCS Seminar: 3 August 2021 - William J. Bowman

Title: Compilation as Multi-Language Semantics

Abstract:

Modelling interoperability between programs in different languages is a key problem when modelling verified and secure compilation, which has been successfully addressed using multi-language semantics.  Unfortunately, existing models of compilation using multi-language semantics define two variants of each compiler pass: a syntactic translation on open terms to model compilation, and a run-time translation of closed terms at multi-language boundaries to model interoperability.

In this talk, I discuss work-in-progress approach to uniformly model a compiler entirely as a reduction system on open term in a multi-language semantics, rather than as a syntactic translation.  This simultaneously defines the compiler and the interoperability semantics, reducing duplication.  It also provides interesting semantic insights.  Normalization of the cross-language redexes performs ahead-of-time (AOT) compilation.  Evaluation in the multi-language models just-in-time (JIT) compilation.  Confluence of multi-language reduction implies compiler correctness, and part of the secure compilation proof (full abstraction), enabling focus on the difficult part of the proof.  Subject reduction of the multi-language reduction implies type-preservation of the compiler.  

Bio: William J. Bowman is an Assistant Professor of computer science in the software Practices Lab at University of British Columbia.  Broadly speaking, he is interested in making it easier for programmers to communicate their intent to machines, and preserving that intent through compilation.  More specifically, his research interests include secure and verified compilation, dependently typed programming, verification, meta-programming, and interoperability. is recent work examines type-preserving compilation of dependently yped programming languages like Coq, a technique that can enable preserving security and correctness invariants of verified software through compilation and statically enforcing those invariants in the low-level (assembly-like) code generated by compilers.