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
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

14:00 - 15:40
Functional Programming and CorrectnessPLDI Research Papers at Aula Master
Chair(s): Francesco LogozzoFacebook
14:00
25m
Talk
Compiling without continuations
PLDI Research Papers
Luke MaurerUniversity of Oregon, USA, Paul DownenUniversity of Oregon, USA, Zena M. AriolaUniversity of Oregon, USA, Simon Peyton JonesMicrosoft Research, Cambridge
Media Attached
14:25
25m
Talk
FunTAL: Reasonably Mixing a Functional Language with Assembly
PLDI Research Papers
Daniel PattersonNortheastern University, Jamie PercontiNortheastern University, Christos DimoulasHarvard University, USA, Amal AhmedNortheastern University, USA
Media Attached
14:50
25m
Talk
HoTTSQL: Proving Query Rewrites with Univalent SQL Semantics
PLDI Research Papers
Shumo ChuUniversity of Washington, USA, Konstantin WeitzUniversity of Washington, USA, Alvin CheungUniversity of Washington, Dan SuciuUniversity of Washington
Media Attached
15:15
25m
Talk
Levity Polymorphism
PLDI Research Papers
Richard A. EisenbergBryn Mawr College, USA, Simon Peyton JonesMicrosoft Research, Cambridge
Media Attached