ECOOP 2020
Sun 15 - Tue 17 November 2020 Online Conference
co-located with SPLASH 2020
Sun 15 Nov 2020 21:00 - 21:20 at SPLASH-I - S-2 Chair(s): Atsushi Igarashi, Hidehiko Masuhara
Sun 15 Nov 2020 09:00 - 09:20 at SPLASH-I - S-2 Chair(s): Yu David Liu, Shigeru Chiba

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: Central Time (US & Canada) change

09:00 - 10:20: S-2Research Papers at SPLASH-I +12h
Chair(s): Yu David LiuState University of New York (SUNY) Binghamton, Shigeru ChibaThe University of Tokyo
09:00 - 09:20
Talk
Abstracting gradual referencesSCICO Journal-First
Research Papers
Matías ToroUniversity of Chile, Éric TanterUniversity of Chile
Link to publication DOI Media Attached
09:20 - 09:40
Talk
Don't Panic! Better, Fewer, Syntax Errors for LR Parsers
Research Papers
Lukas DiekmannKing's College London, Laurence TrattKing's College London
Link to publication DOI Pre-print Media Attached
09:40 - 10:00
Talk
Blame for Null
Research Papers
Abel NietoAarhus University, Marianna RapoportUniversity of Waterloo, Gregor RichardsUniversity of Waterloo, Ondřej LhotákUniversity of Waterloo
Link to publication DOI Pre-print Media Attached
10:00 - 10:20
Talk
Perfect is the Enemy of Good: Best-Effort Program Synthesis
Research Papers
Hila PelegUniversity of California at San Diego, Nadia PolikarpovaUniversity of California at San Diego
Link to publication DOI Media Attached
21:00 - 22:20: S-2Research Papers at SPLASH-I
Chair(s): Atsushi IgarashiKyoto University, Japan, Hidehiko MasuharaTokyo Institute of Technology
21:00 - 21:20
Talk
Abstracting gradual referencesSCICO Journal-First
Research Papers
Matías ToroUniversity of Chile, Éric TanterUniversity of Chile
Link to publication DOI Media Attached
21:20 - 21:40
Talk
Don't Panic! Better, Fewer, Syntax Errors for LR Parsers
Research Papers
Lukas DiekmannKing's College London, Laurence TrattKing's College London
Link to publication DOI Pre-print Media Attached
21:40 - 22:00
Talk
Blame for Null
Research Papers
Abel NietoAarhus University, Marianna RapoportUniversity of Waterloo, Gregor RichardsUniversity of Waterloo, Ondřej LhotákUniversity of Waterloo
Link to publication DOI Pre-print Media Attached
22:00 - 22:20
Talk
Perfect is the Enemy of Good: Best-Effort Program Synthesis
Research Papers
Hila PelegUniversity of California at San Diego, Nadia PolikarpovaUniversity of California at San Diego
Link to publication DOI Media Attached