FunTAL: Reasonably mixing a functional language with assembly

Daniel Patterson, Jamie Perconti, Christos Dimoulas, Amal Ahmed

Research output: Chapter in Book/Report/Conference proceedingConference contribution

10 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. Copyright is held by the owner/author(s).

Original languageEnglish (US)
Title of host publicationPLDI 2017 - Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation
EditorsAlbert Cohen, Martin Vechev
PublisherAssociation for Computing Machinery
Pages495-509
Number of pages15
ISBN (Electronic)9781450349888
DOIs
StatePublished - Jun 14 2017
Event38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017 - Barcelona, Spain
Duration: Jun 18 2017Jun 23 2017

Publication series

NameProceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)
VolumePart F128414

Other

Other38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017
CountrySpain
CityBarcelona
Period6/18/176/23/17

Keywords

  • Contextual equivalence
  • Inline assembly
  • Logical relations
  • Multi-language semantics
  • Typed assembly language

ASJC Scopus subject areas

  • Software

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

Cite this