FunTAL: Reasonably Mixing a Functional Language with Assembly

TL;DR

FunTAL introduces a formal multi-language system that enables safe interoperability and compositional reasoning between high-level functional languages and low-level assembly, addressing the challenge of bridging their semantic differences.

Contribution

It is the first system to formalize safe interoperability and reasoning between a high-level functional language and assembly, supporting compositional components and mixed-language reasoning.

Findings

Supports reasoning about equivalence of high-level and assembly components

Enables mixed-language programs with callbacks

Handles assembly components with varying basic blocks

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.