SPLASH 2022
Mon 5 - Sat 10 December 2022 Auckland, New Zealand
Fri 9 Dec 2022 11:00 - 11:30 at Seminar Room G007 - Semantics and Security Chair(s): Derek Dreyer

Graduality and parametricity have proven to be extremely challenging notions to bring together. Intuitively, enforcing parametricity gradually requires possibly sealing values in order to detect violations of uniform behavior. Toro et al. (2019) argue that the two notions are incompatible in the context of System F, where sealing is transparently driven by potentially imprecise type information, while New et al. (2020) reconcile both properties at the cost of abandoning the syntax of System F and requiring user-provided sealing annotations that are not subject to graduality guarantees. Furthermore, all current proposals rely on a global form of dynamic sealing in order to enforce parametric behavior at runtime, which weakens parametric reasoning and breaks equivalences in the static language. Based on the observation that the tension between graduality and parametricity comes from the early commitment to seal values based on type information, we propose plausible sealing as a new intermediate language mechanism that allows postponing such decisions to runtime. We propose an intermediate language for gradual parametricity, Funky, which supports plausible sealing in a simplified setting where polymorphism is restricted to instantiations with base and variable types. We prove that Funky satisfies both parametricity and graduality, mechanizing key lemmas in Agda. Additionally, we avoid global dynamic sealing and instead propose a novel lexically-scoped form of sealing realized using a representation of evidence inspired by the category of spans. As a consequence, Funky satisfies a standard formulation of parametricity that does not break System F equivalences. In order to show the practicality of plausible sealing, we describe a translation from Funk, a source language without explicit sealing, to Funky, that takes care of inserting plausible sealing forms. We establish graduality of Funk, subject to a restriction on type applications, and explain the source-level parametric reasoning it supports. Finally, we provide an interactive prototype along with illustrative examples both novel and from the literature.

Fri 9 Dec

Displayed time zone: Auckland, Wellington change

10:30 - 12:00
Semantics and SecurityOOPSLA at Seminar Room G007
Chair(s): Derek Dreyer MPI-SWS
10:30
30m
Research paper
Le Temps des Cerises: Efficient Temporal Stack Safety on Capability Machines using Directed CapabilitiesDistinguished Paper
OOPSLA
Aina Linn Georges Aarhus University, Alix Trieu ANSSI, Lars Birkedal Aarhus University
DOI
11:00
30m
Research paper
Plausible sealing for gradual parametricity
OOPSLA
Elizabeth Labrada University of Chile, Matías Toro University of Chile, Éric Tanter University of Chile, Dominique Devriese KU Leuven
DOI
11:30
30m
Research paper
Purity of an ST monad: full abstraction by semantically typed back-translation
OOPSLA
Koen Jacobs KU Leuven, Dominique Devriese KU Leuven, Amin Timany Aarhus University
DOI