ECOOP 2020
Sun 15 - Tue 17 November 2020 Online Conference
co-located with SPLASH 2020
Mon 16 Nov 2020 17:00 - 17:20 at SPLASH-III - M-6B Chair(s): Raffi Khatchadourian, Patrick Rein
Tue 17 Nov 2020 05:00 - 05:20 at SPLASH-III - M-6B Chair(s): Patrick Rein, Manuel Serrano

Herman et al. (2007, 2010) pointed out that the insertion of run-time checks into a gradually typed program could hamper tail-call optimization and, as a result, worsen the space complexity of the program. To address the problem, they proposed a space-efficient coercion calculus, which was subsequently improved by Garcia, et al. (2009) and Siek et al. (2015). The semantics of these calculi involves eager composition of run-time checks expressed by coercions to prevent the size of a term from growing. However, it relies also on a nonstandard reduction rule, which does not seem easy to implement. In fact, no compiler implementation of gradually typed languages fully supports the space-efficient semantics faithfully.

In this paper, we study coercion-passing style, which Herman et al. have already mentioned, as a technique for straightforward space-efficient implementation of gradually typed languages. A program in coercion-passing style passes “the rest of run-time checks” around—just like continuation-passing style (CPS), in which “the rest of computation” has been passed around—and (unlike CPS) composes coercions eagerly. We give a formal coercion-passing translation from $\lambda$S by Siek et al. to $\lambda$S$_1$, which is a new calculus of first-class coercions tailored for coercion-passing style, and prove correctness of the translation. We also implement our coercion-passing style transformation for the Grift compiler developed by Kuhlenschmidt et al. and give an experimental result.

#### Conference DayMon 16 NovDisplayed time zone: Central Time (US & Canada) change

 17:00 - 17:20 M-6BResearch Papers at SPLASH-III +12h Chair(s): Raffi KhatchadourianCity University of New York, Patrick ReinHasso Plattner Institute 17:0020mTalk Space-Efficient Gradual Typing in Coercion-Passing StyleResearch PapersYuya TsudaKyoto University, Atsushi IgarashiKyoto University, Japan, Tomoya TabuchiKyoto University Link to publication DOI Media Attached

#### Conference DayTue 17 NovDisplayed time zone: Central Time (US & Canada) change

 05:00 - 05:20 M-6BResearch Papers at SPLASH-III Chair(s): Patrick ReinHasso Plattner Institute, Manuel SerranoInria, France 05:0020mTalk Space-Efficient Gradual Typing in Coercion-Passing StyleResearch PapersYuya TsudaKyoto University, Atsushi IgarashiKyoto University, Japan, Tomoya TabuchiKyoto University Link to publication DOI Media Attached