ECOOP 2020
Sun 15 - Tue 17 November 2020 Online Conference
co-located with SPLASH 2020
Sun 15 Nov 2020 21:00 - 21:20 at OOPSLA/ECOOP - S-2
Sun 15 Nov 2020 09:00 - 09:20 at OOPSLA/ECOOP - S-2

Gradual typing is an effective approach to integrate static and dynamic typing, which supports the smooth transition between both extremes via the imprecision of type annotations. Gradual typing has been applied in many scenarios such as objects, subtyping, effects, ownership, typestates, information-flow typing, parametric polymorphism, etc. In particular, the combination of gradual typing and mutable references has been explored by different authors, giving rise to four different semantics—invariant, guarded, monotonic and permissive references. These semantics were specially crafted to reflect different design decisions with respect to precision and efficiency tradeoffs. Since then, progress has been made in the formulation of methodologies to systematically derive gradual counterparts of statically-typed languages, but these have not been applied to study mutable references.

In this article, we explore how the Abstracting Gradual Typing (AGT) methodology, which has been shown to be effective in a variety of settings, applies to mutable references. Starting from a standard statically-typed language with references, we systematically derive with AGT a novel gradual language, called λREF˜. We establish the properties of λREF˜; in particular, it is the first gradual language with mutable references that is proven to satisfy the gradual guarantee. We then compare λREF˜ with the main four existing approaches to gradual references, and show that the application of AGT does justify one of the proposed semantics: we formally prove that the treatment of references in λREF˜ corresponds to the guarded semantics, by presenting a bisimilation with the coercion semantics of Herman et al. In the process, we uncover that any direct application of AGT yields a gradual language that is not space-efficient. We consequently adjust the dynamic semantics of λREF˜ to recover space efficiency. We then show how to extend λREF˜ to support both monotonic and permissive references as well. Finally, we provide the first proof of the dynamic gradual guarantee for monotonic references. As a result, this paper sheds further light on the design space of gradual languages with mutable references and contributes to deepening the understanding of the AGT methodology.

Sun 15 Nov
Times are displayed in time zone: (GMT-05:00) Central Time (US & Canada) change

09:00 - 10:20: S-2Research Papers at OOPSLA/ECOOP +12h
09:00 - 09:20
Talk
Research Papers
Matías ToroUniversity of Chile, Éric TanterUniversity of Chile
DOI
09:20 - 09:40
Talk
Research Papers
Lukas DiekmannKing's College London, Laurence TrattKing's College London
Pre-print
09:40 - 10:00
Talk
Research Papers
Abel NietoAarhus University, Marianna RapoportUniversity of Waterloo, Gregor RichardsUniversity of Waterloo, Ondřej LhotákUniversity of Waterloo
Pre-print
10:00 - 10:20
Talk
Research Papers
Hila PelegUniversity of California, San Diego, Nadia PolikarpovaUniversity of California, San Diego
21:00 - 22:20: S-2Research Papers at OOPSLA/ECOOP
21:00 - 21:20
Talk
Research Papers
Matías ToroUniversity of Chile, Éric TanterUniversity of Chile
DOI
21:20 - 21:40
Talk
Research Papers
Lukas DiekmannKing's College London, Laurence TrattKing's College London
Pre-print
21:40 - 22:00
Talk
Research Papers
Abel NietoAarhus University, Marianna RapoportUniversity of Waterloo, Gregor RichardsUniversity of Waterloo, Ondřej LhotákUniversity of Waterloo
Pre-print
22:00 - 22:20
Talk
Research Papers
Hila PelegUniversity of California, San Diego, Nadia PolikarpovaUniversity of California, San Diego