[an error occurred while processing this directive]
An error occured whilst processing this directive
Space-Efficient Blame Tracking for Gradual Typing
University of Colorado, Boulder
11am Monday, 23rd of March, 2009
Room 4.31/4.33, Informatics Forum
Abstract
Gradual typing combines static and dynamic typing in the same
language, giving the programmer fine-grained control over how much of
a program is statically typed. For gradual typing to be practical, the
system should report sources of run-time type errors (i.e., perform
blame tracking) and the space overhead should be limited to a constant
factor. Wadler and Findler's blame calculus demonstrates how to
perform blame tracking and comes with a blame theorem that statically
characterizes which coercions are safe from blame. Herman, Tomb, and
Flanagan, on the other hand, show how to achieve space efficiency
using Henglein's coercion calculus. This talk weaves together these
two lines of research, showing how to perform space-efficient blame
tracking. The talk also presents a new blame tracking strategy whose
safe coercions are characterized by the traditional subtyping
relation. Last but not least, the talk presents a modular semantic
framework that instantiates a number of space-efficient,
blame-tracking calculi, varying in what errors they detect and how
they assign blame. Two of the resulting calculi extend work from the
literature with blame tracking or space efficiency and two of the
resulting calculi are new.
An error occured whilst processing this directive