William J Bowman: Compilation as Multi Language Semantics

Abstract:

Modeling interoperability between programs in different languages is
a key problem when modeling 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.
His recent work examines type-preserving compilation of dependently
typed 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.

(Joint seminar with the University of Glasgow's PLUG series: http://www.dcs.gla.ac.uk/plug/ )

WilliamBowman:Compilation