Thu 16 Jun 2016 10:30 - 11:00 at Grand Ballroom San Rafael - Types I Chair(s): David Walker

Unhandled exceptions crash programs, so a compile-time check that exceptions are handled should in principle make software more reliable. But designers of some recent languages have argued that the benefits of statically checked exceptions are not worth the costs. We introduce a new statically checked exception mechanism that addresses the problems with existing checked-exception mechanisms. In particular, it interacts well with higher-order functions and other design patterns. The key insight is that whether an exception should be treated as a “checked” exception is not a property of its type but rather of the context in which the exception propagates. Statically checked exceptions can “tunnel” through code that is oblivious to their presence, but the type system nevertheless checks that these exceptions are handled. Further, exceptions can be tunneled without being accidentally caught, by expanding the space of exception identifiers to identify the exception-handling context. The resulting mechanism is expressive and syntactically light, and can be implemented efficiently. We demonstrate the expressiveness of the mechanism using significant codebases and evaluate its performance. We have implemented this new exception mechanism as part of the new Genus programming language, but the mechanism could equally well be applied to other programming languages.

Thu 16 Jun
Times are displayed in time zone: Tijuana, Baja California change

10:30 - 12:00: Types IResearch Papers at Grand Ballroom San Rafael
Chair(s): David WalkerPrinceton University
10:30 - 11:00
Accepting Blame for Safe Tunneled Exceptions
Research Papers
Yizhou ZhangCornell University, Guido SalvaneschiTU Darmstadt, Quinn BeightolCornell, Barbara LiskovMIT, Andrew C. MyersCornell University
Link to publication DOI Media Attached
11:00 - 11:30
Occurrence Typing Modulo Theories
Research Papers
Andrew KentIndiana University, David Kempe II, Sam Tobin-HochstadtIndiana University
Pre-print Media Attached
11:30 - 12:00
Refinement Types for TypeScript
Research Papers
Panagiotis VekrisUniversity of California, San Diego, Benjamin CosmanUniversity of California, San Diego, Ranjit JhalaUniversity of California, San Diego
Media Attached