SPLASH 2020
Sun 15 - Sat 21 November 2020 Online Conference
Tue 17 Nov 2020 09:40 - 10:00 at SPLASH-I - T-2 Chair(s): Karim Ali, Aritra Sengupta
Tue 17 Nov 2020 21:40 - 22:00 at SPLASH-I - T-2 Chair(s): Iulian Neamtiu, Yaoda Zhou

Pressed by the difficulty of writing asynchronous, event-driven code, mainstream languages have recently been building in support for a variety of advanced control-flow features. Meanwhile, experimental language designs have suggested effect handlers as a unifying solution to programmer-defined control effects, subsuming exceptions, generators, and async–await. However, despite these trends, complex control flow—in particular, control flow that exhibits a bidirectional pattern—remains challenging to manage.

We introduce bidirectional algebraic effects, a new programming abstraction that supports bidirectional control transfer in a more natural way. Handlers of bidirectional effects can raise further effects to transfer control back to the site where the initiating effect was raised, and can use themselves to handle their own effects. We present applications of this expressive power, which falls out naturally as we push toward the unification of effectful programming with object-oriented programming. We pin down the mechanism and the unification formally using a core language that makes generalizations to effect operations and effect handlers.

The usual propagation semantics of control effects such as exceptions conflicts with modular reasoning in the presence of effect polymorphism—it breaks parametricity. Bidirectionality exacerbates the problem. Hence, we set out to show the core language, which builds on the existing tunneling semantics for algebraic effects, is not only type-safe (no effects go unhandled), but also abstraction-safe (no effects are accidentally handled). We devise a step-indexed logical-relations model, and construct its parametricity and soundness proofs. These core results are fully mechanized in Coq. While a full-featured compiler is left to future work, experiments show that as a first-class language feature, bidirectional handlers can be implemented efficiently.

Tue 17 Nov
Times are displayed in time zone: Central Time (US & Canada) change

09:00 - 10:20: T-2OOPSLA at SPLASH-I +12h
Chair(s): Karim AliUniversity of Alberta, Aritra SenguptaAmazon Web Services, USA
09:00 - 09:20
Talk
Formulog: Datalog for SMT-Based Static Analysis
OOPSLA
Aaron BembenekHarvard University, Michael GreenbergPomona College, Stephen ChongHarvard University
Link to publication DOI Media Attached
09:20 - 09:40
Talk
A Large-Scale Longitudinal Study of Flaky Tests
OOPSLA
Wing LamUniversity of Illinois at Urbana-Champaign, Stefan WinterTU Darmstadt, Anjiang WeiPeking University, Tao XiePeking University, Darko MarinovUniversity of Illinois at Urbana-Champaign, Jonathan BellNortheastern University
Link to publication DOI Media Attached
09:40 - 10:00
Talk
Handling Bidirectional Control Flow
OOPSLA
Yizhou ZhangUniversity of Waterloo, Guido SalvaneschiUniversity of St. Gallen, Andrew C. MyersCornell University
Link to publication DOI Media Attached
10:00 - 10:20
Talk
WATCHER: In-Situ Failure Diagnosis
OOPSLA
Hongyu LiuPurdue University, Sam SilvestroUniversity of Texas at San Antonio, Xiangyu ZhangPurdue University, Jian HuangUniversity of Illinois at Urbana-Champaign, Tongping LiuUniversity of Massachusetts at Amherst
Link to publication DOI Media Attached
21:00 - 22:20: T-2OOPSLA at SPLASH-I
Chair(s): Iulian NeamtiuNew Jersey Institute of Technology, Yaoda ZhouUniversity of Hong Kong
21:00 - 21:20
Talk
Formulog: Datalog for SMT-Based Static Analysis
OOPSLA
Aaron BembenekHarvard University, Michael GreenbergPomona College, Stephen ChongHarvard University
Link to publication DOI Media Attached
21:20 - 21:40
Talk
A Large-Scale Longitudinal Study of Flaky Tests
OOPSLA
Wing LamUniversity of Illinois at Urbana-Champaign, Stefan WinterTU Darmstadt, Anjiang WeiPeking University, Tao XiePeking University, Darko MarinovUniversity of Illinois at Urbana-Champaign, Jonathan BellNortheastern University
Link to publication DOI Media Attached
21:40 - 22:00
Talk
Handling Bidirectional Control Flow
OOPSLA
Yizhou ZhangUniversity of Waterloo, Guido SalvaneschiUniversity of St. Gallen, Andrew C. MyersCornell University
Link to publication DOI Media Attached
22:00 - 22:20
Talk
WATCHER: In-Situ Failure Diagnosis
OOPSLA
Hongyu LiuPurdue University, Sam SilvestroUniversity of Texas at San Antonio, Xiangyu ZhangPurdue University, Jian HuangUniversity of Illinois at Urbana-Champaign, Tongping LiuUniversity of Massachusetts at Amherst
Link to publication DOI Media Attached