On the Cost of Type-Tag Soundness
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 JanDisplayed time zone: Tijuana, Baja California change
14:00 - 15:30
|A Guess-and-Assume Approach to Loop Fusion for Program Verification
Akifumi Imanishi Kyoto University, Kohei Suenaga Graduate School of Informatics, Kyoto University, Atsushi Igarashi Kyoto University, JapanDOI
|Gradually Typed Symbolic Expressions
|On the Cost of Type-Tag Soundness