FunTAL: Reasonably Mixing a Functional Language with Assembly
Abstract
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.
Cite
@article{arxiv.1711.03871,
title = {FunTAL: Reasonably Mixing a Functional Language with Assembly},
author = {Daniel Patterson and Jamie Perconti and Christos Dimoulas and Amal Ahmed},
journal= {arXiv preprint arXiv:1711.03871},
year = {2017}
}
Comments
15 pages; implementation at https://dbp.io/artifacts/funtal/; published in PLDI '17, Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, June 18 - 23, 2017, Barcelona, Spain