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 Jan Times are displayed in time zone: Tijuana, Baja California change
|14:00 - 14:30|
|A Guess-and-Assume Approach to Loop Fusion for Program Verification|
Akifumi ImanishiKyoto University, Kohei SuenagaGraduate School of Informatics, Kyoto University, Atsushi IgarashiKyoto University, JapanDOI
|14:30 - 15:00|
|Gradually Typed Symbolic Expressions|
|15:00 - 15:30|
|On the Cost of Type-Tag Soundness|