Compositional compiler verification aims to ensure correct compilation of components, not just whole programs. Perconti and Ahmed [2014] propose a methodology for compositional compiler correctness that supports linking with code of arbitrary provenance. In particular, they allow compiled components to be linked with code whose functionality cannot even be expressed in the compiler's own source language. The essence of their approach is to define a multi-language system that formalizes interoperability between the source and target languages so that compiler correctness can be stated as contextual equivalence in the multi-language. They illustrate this methodology on a two-pass type-preserving compiler for a polymorphic language with recursive types.

We present FunTAL, the first multi-language system to formalize safe interoperability between a high-level functional language and low-level assembly code while supporting compositional reasoning about the mix. A central challenge in developing such a multi-language is bridging the gap between assembly, which is staged into jumps to continuations, and high-level code, where subterms return a result. We present a compositional stack-based typed assembly language that supports components, comprised of one or more basic blocks, that may be embedded in high-level contexts. We also present a logical relation for FunTAL that supports reasoning about equivalence of high-level components and their assembly replacements, mixed-language programs with callbacks between languages, and assembly components comprised of different numbers of basic blocks.