FunTAL: Reasonably Mixing a Functional Language with Assembly
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.
Tue 20 Jun
|14:00 - 14:25|
Luke MaurerUniversity of Oregon, USA, Paul DownenUniversity of Oregon, USA, Zena M. AriolaUniversity of Oregon, USA, Simon Peyton JonesMicrosoft Research, CambridgeMedia Attached
|14:25 - 14:50|
Daniel PattersonNortheastern University, Jamie PercontiNortheastern University, Christos DimoulasHarvard University, USA, Amal AhmedNortheastern University, USAMedia Attached
|14:50 - 15:15|
Shumo ChuUniversity of Washington, USA, Konstantin WeitzUniversity of Washington, USA, Alvin CheungUniversity of Washington, Dan SuciuUniversity of WashingtonMedia Attached
|15:15 - 15:40|