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 how to bridge the gap between assembly, which is staged into calls 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.

This work is a first step towards multi-language formalisms that (1) allow developers to replace high-level components with performant low-level implementations while reasoning about safety and correctness of the replacement; (2) can be used to specify compiler correctness theorems that permit compiled components to be linked with low-level code compiled from other languages (as proposed by Perconti and Ahmed [1, 19]); and (3) can be used to verify just-in-time compilers which replace portions of high-level code with equivalent assembly, inserting callbacks back to high-level code.