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
Times are displayed in time zone: Osaka, Sapporo, Tokyo change

15:15 - 16:30: Session 3Research Papers at Noh Theater
Chair(s): Neel KrishnaswamiUniversity of Birmingham, UK
15:15 - 15:40
Talk
Fully Abstract Compilation via Universal Embedding
Research Papers
Max NewNortheastern University, William J. BowmanNortheastern University, Amal AhmedNortheastern University
DOI
15:40 - 16:05
Talk
Oh Lord, Please Don't Let Contracts Be Misunderstood (Functional Pearl)
Research Papers
Christos DimoulasHarvard University, Max NewNortheastern University, Robby FindlerNorthwestern University, Matthias FelleisenNortheastern University
DOI
16:05 - 16:30
Talk
A Type Theory for Incremental Computational Complexity with Control Flow Changes
Research Papers
Ezgi ÇiçekMPI-SWS, Germany, Zoe ParaskevopoulouPrinceton University, USA, Deepak GargMPI-SWS, Germany
DOI