Building and using pluggable type systems

Are you a practitioner who is tired of null pointer exceptions, unintended side effects, SQL injections, concurrency errors, mistaken equality tests, and other run-time errors that appear during testing or in the field? A pluggable type system can guarantee the absence of these errors, and many more. Are you a researcher who wants to be able to quickly and easily implement a type system, giving you the ability to evaluate it in practice and to field it? You need a framework that supports these essential activities. This demo is aimed at both audiences. It describes both the theory of pluggable types and also the practice of implementing them. A simple pluggable type-checker can be implemented in 2 minutes, and can be enhanced thereafter. A type checkers is easy to create, easy for programmers to use, and effective in finding real, important bugs. The demo uses the Checker Framework, which enables you to create pluggable type systems for Java, while your code remains backward-compatible with all versions of Java. The ideas translate to other languages and toolsets. The tools are freely available at http://types.cs.washington.edu/checker-framework/.