FunTAL: Reasonably mixing a functional language with assembly

Daniel Patterson, Jamie Perconti, Christos Dimoulas, Amal Ahmed

Research output: Contribution to journalArticle

2 Scopus citations

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.

Original languageEnglish (US)
Pages (from-to)495-509
Number of pages15
JournalACM SIGPLAN Notices
Volume52
Issue number6
DOIs
StatePublished - Jun 14 2017
Externally publishedYes

Keywords

  • contextual equivalence
  • inline assembly
  • logical relations
  • multi-language semantics
  • typed assembly language

ASJC Scopus subject areas

  • Computer Science(all)

Fingerprint Dive into the research topics of 'FunTAL: Reasonably mixing a functional language with assembly'. Together they form a unique fingerprint.

  • Cite this