BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Fast run-time type checking for whole programs - Stephen Kell (Uni
 versity of Lugano)
DTSTART:20121122T160000Z
DTEND:20121122T170000Z
UID:TALK39482@talks.cam.ac.uk
CONTACT:Eiko Yoneki
DESCRIPTION:Despite a wealth of literature\, dynamically detecting type er
 rors 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)\, l
 ack of binary compatibility (hindering use of libraries)\, high run-time o
 verhead\, and/or reliance on conservative static reasoning. Revisiting thi
 s 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 instrume
 nts unmodified C source code with appropriate assertions.\nThe decision to
  encode type checks as "ordinary" assertions has some interesting conseque
 nces. I will discuss some of these\, including a sketched approach for ext
 ending the system towards static checking using symbolic execution.  I wil
 l try to convince the audience that this can offer greatly improved flexib
 ility over conventional syntax-directed type checkers.\n\nBio: Stephen Kel
 l is a postdoctoral researcher at the University of Lugano\, Switzerland. 
 He completed his PhD in the Networks and Operating Systems group at the Un
 iversity of Cambridge\, and also held a postdoctoral position at the Unive
 rsity of Oxford. His interests include many aspects of programming languag
 es\, operating systems\, and software engineering\; a recurring theme is i
 mproving the productivity of programmers.\n
LOCATION:FW26\, Computer Laboratory\, William Gates Builiding
END:VEVENT
END:VCALENDAR