[Pl-seminar] 11/30: Amal Ahmed, "An Equivalence-Preserving CPS Translation via Multi-Language Semantics"

[Aaron Turon]

NEU Programming Languages Seminar presents

Amal Ahmed
Northeastern University

Wednesday, 11/30

11:45am - 1:30pm
Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

An Equivalence-Preserving CPS Translation via Multi-Language Semantics

In a nutshell...

This talk is about *equivalence-preserving* compilation: what that
property is, why we might want it, why it's hard to achieve and even
harder to prove, and the outline of a strategy (illustrated by
considering a simple CPS translation) that I think can scale to
equivalence-preserving compilation of "full-featured" languages.

In more detail...

Language-based security relies on the assumption that all potential
attacks follow the rules of the language in question.  When
programs are compiled into a different language, this is true only if
the translation process preserves observational equivalence.

To prove that a translation preserves equivalence, one must show that
if two program fragments cannot be distinguished by any source
context, then their translations cannot be distinguished by any target
context.  Informally, target contexts must be no more powerful than
source contexts, i.e., for every target context there exists a source
context that ``behaves the same.''  This seems to amount to being able
to ``back-translate'' arbitrary target terms.  However, that is simply
not viable for practical compilers where the target language is
lower-level and, thus, contains expressions that have no source
equivalent.

In this work, we give a CPS translation from a less expressive source
language (STLC) to a more expressive target language (System F) and
prove that the translation preserves observational equivalence.  The
key to our equivalence-preserving compilation is the choice of the
right type translation: a source type S mandates a set of behaviors
and we must ensure that its translation S^+ mandates semantically
equivalent behaviors at the target level.  Based on this type
translation, we demonstrate how to prove that for every target term of
type S^+, there exists an equivalent source term of type S --- even
when sub-terms of the target term are not necessarily ``back-translatable''
themselves.  A key novelty of our proof, resulting in a pleasant proof
structure, is that it leverages a multi-language semantics where source
and target terms may interoperate.

The paper appeared at ICFP'11:
http://www.cs.indiana.edu/~amal/papers/epc/main.pdf