Abstract

Despite a wealth of literature, dynamically detecting type errors in unsafe code has so far only been addressed by approaches suffering one or more common weaknesses: language-specificity (typically for C only), lack of source compatibility (requiring a modified source dialect), lack of binary compatibility (hindering use of libraries), high run-time overhead, and/or reliance on conservative static reasoning. Revisiting this problem, I present a simple and fast encoding of run-time type checking as assertions, together with a run-time infrastructure which allows fast evaluation of these assertions, and a prototype front-end which instruments unmodified C source code with appropriate assertions. The decision to encode type checks as “ordinary” assertions has some interesting consequences. I will discuss some of these, including a sketched approach for extending the system towards static checking using symbolic execution. I will try to convince the audience that this can offer greatly improved flexibility over conventional syntax-directed type checkers.

Bio: Stephen Kell is a postdoctoral researcher at the University of Lugano, Switzerland. He completed his PhD in the Networks and Operating Systems group at the University of Cambridge, and also held a postdoctoral position at the University of Oxford. His interests include many aspects of programming languages, operating systems, and software engineering; a recurring theme is improving the productivity of programmers.