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

Displayed time zone: Tijuana, Baja California change

13:40 - 15:20
Outside the boxResearch Papers at Watercourt
Chair(s): Lars Birkedal Aarhus University
13:40
25m
Talk
Go with the Flow: Compositional Abstractions for Concurrent Data Structures
Research Papers
Siddharth Krishna New York University, Dennis Shasha New York University, Thomas Wies New York University
14:05
25m
Talk
Parametricity versus the Universal Type
Research Papers
Dominique Devriese KU Leuven, Marco Patrignani Saarland University, CISPA, Frank Piessens KU Leuven
14:30
25m
Talk
Linearity in Higher-Order Recursion Schemes
Research Papers
Pierre Clairambault CNRS & ENS Lyon, Charles Grellois INRIA Sophia Antipolis & Aix-Marseille Université, Andrzej Murawski University of Oxford
14:55
25m
Talk
Symbolic Types for Lenient Symbolic Execution
Research Papers
Stephen Chang Northeastern University, Alex Knauth Northeastern University, Emina Torlak University of Washington