Recent research has identified significant performance hurdles that sound gradual typing needs to overcome (Takikawa et al. 2016). These performance hurdles stem from the fact that the run-time checks gradual type systems insert into code can cause a lot of overhead. We propose a small sacrifice in flexibility that enables us to implement efficient checks. We formalize the core of a nominal object-oriented language that fulfills a variety of desirable properties for gradually typed languages, and present evidence that an implementation of this language suffers minimal overhead even in adversarial benchmarks identified in earlier work, while achieving good overall performance.
Wed 25 OctDisplayed time zone: Tijuana, Baja California change
Wed 25 Oct
Displayed time zone: Tijuana, Baja California change
13:30 - 15:00 | |||
13:30 22mTalk | Sound Gradual Typing: Only Mostly Dead OOPSLA Spenser Andrew Bauman Indiana University, USA, Sam Tobin-Hochstadt Indiana University, Jeremy G. Siek Indiana University, USA, CF Bolz-Tereick DOI | ||
13:52 22mTalk | Sound Gradual Typing Is Nominally Alive and Well OOPSLA DOI | ||
14:15 22mTalk | The VM Already Knew That: Leveraging Compile-Time Knowledge to Optimize Gradual Typing OOPSLA Gregor Richards University of Waterloo, Ellen Arteca University of Waterloo, Canada, Alexi Turcotte University of Waterloo DOI | ||
14:37 22mTalk | Model Checking Copy Phases of Concurrent Copying Garbage Collection with Various Memory Models OOPSLA Tomoharu Ugawa Kochi University of Technology, Japan, Tatsuya Abe Chiba Institute of Technology, Japan, Toshiyuki Maeda Chiba Institute of Technology, Japan DOI |