Mon 8 Jan 2018 15:00 - 15:30 at Crocker - Session 1-2 Chair(s): Kenichi Asai

Gradual typing systems ensure type soundness by transforming static type annotations into run-time checks. These checks provide semantic guarantees, but may come at a large cost in performance. In particular, recent work by Takikawa et al. suggests that enforcing a conventional form of type soundness may slow a program by two orders of magnitude.

Since different gradual typing systems satisfy different notions of soundness, the question then arises: what is the cost of such varying notions of soundness? This paper answers an instance of this question by applying Takikawa et al.’s evaluation method to Reticulated Python, which satisfies a notion of type-tag soundness. We find that the cost of soundness in Reticulated is at most one order of magnitude.

Mon 8 Jan

Displayed time zone: Tijuana, Baja California change

14:00 - 15:30
Session 1-2PEPM at Crocker
Chair(s): Kenichi Asai Ochanomizu University
14:00
30m
Talk
A Guess-and-Assume Approach to Loop Fusion for Program Verification
PEPM
Akifumi Imanishi Kyoto University, Kohei Suenaga Graduate School of Informatics, Kyoto University, Atsushi Igarashi Kyoto University, Japan
DOI
14:30
30m
Talk
Gradually Typed Symbolic Expressions
PEPM
David Broman KTH Royal Institute of Technology, Jeremy G. Siek Indiana University, USA
DOI
15:00
30m
Talk
On the Cost of Type-Tag Soundness
PEPM
Ben Greenman Northeastern University, Zeina Migeed University of California, Los Angeles
DOI