Write a Blog >>
Wed 20 Jan 2016 14:20 - 14:45 at Grand Bay South - Track 2: Correct Compilation Chair(s): Jens Palsberg

A compiler is fully-abstract if the compilation from source language programs to target language programs preserves and reflects behavioural equivalence. Such compilers have important security benefits, as they limit the power of an attacker interacting with the program in the target language to that of an attacker interacting with the program in the source language. Proving compiler full- abstraction is, however, rather complicated. A common proof technique is based on the back-translation of target-level program con- texts to behaviourally-equivalent source-level contexts. However, constructing such a back-translation is problematic when the source language is not strong enough to embed an encoding of the target language. For instance, when compiling from the simply-typed λ- calculus (λτ ) to the untyped λ-calculus (λu ), the lack of recursive types in λτ prevents such a back-translation. We propose a general and elegant solution for this problem. The key insight is that it suffices to construct an approximate back- translation. The approximation is only accurate up to a certain number of steps and conservative beyond that, in the sense that the context generated by the back-translation may diverge when the original would not, but not vice versa. Based on this insight, we describe a general proof technique for proving compiler full- abstraction and demonstrate it on a compiler from λτ to λu. The proof uses asymmetric cross-language logical relations and makes innovative use of step-indexing to express the relation between a context and its approximate back-translation. We believe this proof technique can scale to challenging settings and enable simpler, more scalable proofs of compiler full-abstraction.

Wed 20 Jan
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

14:20 - 16:00: Track 2: Correct CompilationResearch Papers at Grand Bay South
Chair(s): Jens PalsbergUniversity of California, Los Angeles
14:20 - 14:45
Fully-Abstract Compilation by Approximate Back-Translation
Research Papers
Dominique DevrieseiMinds - Distrinet, KU Leuven, Marco PatrignaniKU Leuven, Frank PiessensiMinds - Distrinet, KU Leuven
Pre-print Media Attached
14:45 - 15:10
Lightweight Verification of Separate Compilation
Research Papers
Jeehoon KangSeoul National University, Yoonseung KimSeoul National University (South Korea), Chung-Kil HurSeoul National University, Derek DreyerMPI-SWS, Viktor VafeiadisMPI-SWS, Germany
Media Attached File Attached
15:10 - 15:35
From MinX to MinC: Semantics-Driven Decompilation of Recursive Datatypes
Research Papers
Media Attached
15:35 - 16:00
Sound Type-dependent Syntactic Language Extension
Research Papers
Florian LorenzenTU Berlin, Sebastian ErdwegTU Darmstadt, Germany
Pre-print Media Attached File Attached