Write a Blog >>
Tue 20 Jun 2017 14:25 - 14:50 at Aula Master - Functional Programming and Correctness Chair(s): Francesco Logozzo

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

pldi-2017-papers
14:00 - 15:40: PLDI Research Papers - Functional Programming and Correctness at Aula Master
Chair(s): Francesco LogozzoFacebook
pldi-2017-papers149796000000014:00 - 14:25
Talk
Luke MaurerUniversity of Oregon, USA, Paul DownenUniversity of Oregon, USA, Zena M. AriolaUniversity of Oregon, USA, Simon Peyton JonesMicrosoft Research, Cambridge
Media Attached
pldi-2017-papers149796150000014:25 - 14:50
Talk
Daniel PattersonNortheastern University, Jamie PercontiNortheastern University, Christos DimoulasHarvard University, USA, Amal AhmedNortheastern University, USA
Media Attached
pldi-2017-papers149796300000014:50 - 15:15
Talk
Shumo ChuUniversity of Washington, USA, Konstantin WeitzUniversity of Washington, USA, Alvin CheungUniversity of Washington, Dan SuciuUniversity of Washington
Media Attached
pldi-2017-papers149796450000015:15 - 15:40
Talk
Richard A. EisenbergBryn Mawr College, USA, Simon Peyton JonesMicrosoft Research, Cambridge
Media Attached