Thu 11 Jan 2018 14:05 - 14:30 at Watercourt - Outside the box Chair(s): Lars Birkedal

There has long been speculation in the scientific literature on how to dynamically enforce parametricity such as that yielded by System F. Almost 20 years ago, Sumii and Pierce proposed a formal compiler from System F into the cryptographic lambda calculus: an untyped lambda calculus extended with an idealised model of encryption. They conjectured that this compiler was fully abstract, i.e. that compiled terms are contextually equivalent if and only if the original terms were, a property that can be seen as a form of secure compilation. The conjecture has received attention in several other publications since then, but remains open to this day.

More recently, several researchers have been looking at gradually-typed languages that extend System~F. In this setting it is natural to wonder whether embedding System F into these gradually-typed languages preserves contextual equivalence and thus parametricity.

In this paper, we answer both questions negatively. We provide a concrete counterexample: two System F terms whose contextual equivalence is not preserved by the Sumii-Pierce compiler, nor the embedding into the polymorphic blame calculus. This counterexample relies on the absence in System F of what we called a ``Universal'' type, i.e., a type where all other types can be injected to and extracted from. As the languages in which System F is compiled have a universal type, the compilation cannot be fully abstract; this paper explains why.

We believe this paper thus sheds light on recent results in the field of gradually typed languages and it provides a perspective for further research into secure compilation of polymorphic languages.

Thu 11 Jan
Times are displayed in time zone: Tijuana, Baja California change

13:40 - 15:20: Outside the boxResearch Papers at Watercourt
Chair(s): Lars BirkedalAarhus University
13:40 - 14:05
Talk
Research Papers
Siddharth KrishnaNew York University, Dennis ShashaNew York University, Thomas WiesNew York University
14:05 - 14:30
Talk
Research Papers
Dominique DevrieseKU Leuven, Marco PatrignaniSaarland University, CISPA, Frank PiessensKU Leuven
14:30 - 14:55
Talk
Research Papers
Pierre ClairambaultCNRS & ENS Lyon, Charles GrelloisINRIA Sophia Antipolis & Aix-Marseille Université, Andrzej MurawskiUniversity of Oxford
14:55 - 15:20
Talk
Research Papers
Stephen ChangNortheastern University, Alex KnauthNortheastern University, Emina TorlakUniversity of Washington