Write a Blog >>
ICFP 2016
Sun 18 - Sat 24 September 2016 Nara, Japan
Mon 19 Sep 2016 15:15 - 15:40 at Noh Theater - Session 3 Chair(s): Neel Krishnaswami

A fully abstract compiler guarantees that two source components are observationally equivalent in the source language if and only if their translations are observationally equivalent in the target. Full abstraction implies the translation is secure: target-language attackers can make no more observations of a compiled component than a source-language attacker interacting with the original source component. Proving full abstraction for realistic compilers is challenging because realistic target languages contain features (such as control effects) unavailable in the source, while proofs of full abstraction require showing that every target context to which a compiled component may be linked can be back-translated to a behaviorally equivalent source context.

We prove the first full abstraction result for a translation whose target language contains exceptions, but the source does not. Our translation—specifically, closure conversion of simply typed λ-calculus with recursive types—uses types at the target level to ensure that a compiled component is never linked with attackers that have more distinguishing power than source-level attackers. We present a new back-translation technique based on a shallow embedding of the target language into the source language at a dynamic type. Then boundaries are inserted that mediate terms between the untyped embedding and the strongly-typed source. This technique allows back-translating non-terminating programs, target features that are untypeable in the source, and well-bracketed effects.

Mon 19 Sep

Displayed time zone: Osaka, Sapporo, Tokyo change

15:15 - 16:30
Session 3Research Papers at Noh Theater
Chair(s): Neel Krishnaswami University of Birmingham, UK
15:15
25m
Talk
Fully Abstract Compilation via Universal Embedding
Research Papers
Max S. New Northeastern University, William J. Bowman Northeastern University, Amal Ahmed Northeastern University
DOI
15:40
25m
Talk
Oh Lord, Please Don't Let Contracts Be Misunderstood (Functional Pearl)
Research Papers
Christos Dimoulas Harvard University, Max S. New Northeastern University, Robert Bruce Findler Northwestern University, Matthias Felleisen Northeastern University
DOI
16:05
25m
Talk
A Type Theory for Incremental Computational Complexity with Control Flow Changes
Research Papers
Ezgi Çiçek MPI-SWS, Germany, Zoe Paraskevopoulou Princeton University, USA, Deepak Garg MPI-SWS, Germany
DOI