Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Thu 21 Jan 2021 19:20 - 19:30 at POPL-B - Types and Functional Languages

Abstracting Gradual Typing (AGT) is a systematic approach to designing gradually-typed languages. Languages developed using AGT automatically satisfy the formal semantic criteria for gradual languages identified by Siek et al. [2015]. Nonetheless, vanilla AGT semantics can still have important shortcomings. First, a gradual language’s runtime checks should preserve the space-efficiency guarantees inherent to the underlying static and dynamic languages. To the contrary, the default operational semantics of AGT break proper tail calls. Second, a gradual language’s runtime checks should enforce basic modular type-based invariants expected from the static type discipline. To the contrary, the default operational semantics of AGT may fail to enforce some invariants in surprising ways. We demonstrate this in the GTFL language of Garcia et al. [2016].

This paper addresses both problems at once by refining the theory underlying AGT’s dynamic checks. Garcia et al. [2016] observe that AGT involves two abstractions of static types: one for the static semantics and one for the dynamic semantics. We recast the latter as an abstract interpretation of subtyping itself, while gradual types still abstract static types. Then we show how forward-completeness [Giacobazzi and Quintarelli 2001] is key to supporting both space-efficient execution and reliable, predictable runtime type enforcement.

Thu 21 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

18:30 - 19:30: Types and Functional LanguagesPOPL at POPL-B
18:30 - 18:40
Talk
Diamonds Are Not Forever: Liveness in Reactive Programming with Guarded Recursion
POPL
Patrick BahrIT University of Copenhagen, Christian Uldal GraulundIT University of Copenhagen, Rasmus Ejlers MøgelbergIT University of Copenhagen
Link to publication DOI
18:40 - 18:50
Talk
On the Semantic Expressiveness of Recursive Types
POPL
Marco PatrignaniStanford University, USA / CISPA, Germany, Eric Mark MartinStanford, Dominique DevrieseVrije Universiteit Brussel
Link to publication DOI
18:50 - 19:00
Talk
Automatic Differentiation in PCF
POPL
Damiano MazzaCNRS, Michele PaganiIRIF - Université de Paris
Link to publication DOI Pre-print
19:00 - 19:10
Talk
Intersection Types and (Positive) Almost-Sure Termination
POPL
Ugo Dal LagoUniversity of Bologna, Italy / Inria, France, Claudia FaggianUniversité de Paris & CNRS, Simona Ronchi Della RoccaUniversity of Torino
Link to publication DOI
19:10 - 19:20
Talk
Intensional Datatype Refinement
POPL
Eddie JonesUniversity of Bristol, Steven RamsayUniversity of Bristol
Link to publication DOI
19:20 - 19:30
Talk
Abstracting Gradual Typing Moving Forward : Precise and Space-Efficient
POPL
Felipe Bañados SchwerterUniversity of British Columbia, Alison M. ClarkUniversity of British Columbia, Khurram A. JaferyUniversity of British Columbia, Ronald GarciaUniversity of British Columbia
Link to publication DOI