Modeling interoperability between programs in different languages is a key problem when modeling compositional 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 are defined: a syntactic translation on open terms, and a run-time translation of closed terms at multi-language boundaries

We introduce a novel 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. Subject reduction of the multi-language reduction implies type-preservation of the compiler. This model provides a strong attacker model through contextual equivalence, retaining its usefulness for modeling secure compilation as full abstraction.

William J. Bowman is an assistant professor of computer science at the University of British Columbia in Vancouver. Broadly speaking, he is interested in making it easier for programmers to communicate their intent to machines, and preserving that intent through the stages of compilation. More specifically, his research interests include secure and verified compilation, dependently typed programming, verification, and meta-programming. His recent work examines type-preserving compilation of dependently typed programming language 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.