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 Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
14:00 - 15:40: Functional Programming and CorrectnessPLDI Research Papers at Aula Master Chair(s): Francesco LogozzoFacebook | |||
14:00 - 14:25 Talk | Compiling without continuations PLDI Research Papers Luke MaurerUniversity of Oregon, USA, Paul DownenUniversity of Oregon, USA, Zena M. AriolaUniversity of Oregon, USA, Simon Peyton JonesMicrosoft Research, Cambridge Media Attached | ||
14:25 - 14:50 Talk | FunTAL: Reasonably Mixing a Functional Language with Assembly PLDI Research Papers Daniel PattersonNortheastern University, Jamie PercontiNortheastern University, Christos DimoulasHarvard University, USA, Amal AhmedNortheastern University, USA Media Attached | ||
14:50 - 15:15 Talk | HoTTSQL: Proving Query Rewrites with Univalent SQL Semantics PLDI Research Papers Shumo ChuUniversity of Washington, USA, Konstantin WeitzUniversity of Washington, USA, Alvin CheungUniversity of Washington, Dan SuciuUniversity of Washington Media Attached | ||
15:15 - 15:40 Talk | Levity Polymorphism PLDI Research Papers Media Attached |