Our tutorial will give attendees the theoretical background and
practical knowledge to use and build scalable, robust, and expressive
pluggable type systems in the context of a realistic object-oriented
programming language. The tutorial will consist of a mix of
activities, both to cater to different learning styles and interests
and to promote alertness throughout the session. We will ask
attendees to bring laptop computers — and a problem of interest to
them — so that they can participate actively throughout the
tutorial.
We will begin with demonstrations of existing checkers in action, both
to show how the checkers support programmer needs and also to show how
the framework enables the creation of effective and usable tools. The
demonstrations will use real code from case studies in which pluggable
type-checkers found important bugs in fielded software. We will
review other results of the case studies, including strengths and
weaknesses of the overall approach. During this component, attendees
will also run the checkers on their own code.
A lecture component will present the theory of type qualifiers. It will
also describe the parts of a pluggable type system.
We will explore the interface that the Checker Framework provides for
implementing a type system. Its cleanly separates distinct tasks:
type qualifiers and hierarchy; type introduction rules; type rules;
and interface to the compiler. It has both declarative and procedural
mechanisms for each of these tasks. In addition to presenting the
interface, we will examine real code from existing checkers. There
are many checkers from which to choose (see supplementary materials)
From the front of the room, we will interactively create a type
checker from scratch at the keyboard. Rather than merely using a
canned demo, we will also take suggestions from the audience regarding
properties to check. This will make the session more interactive and
relevant.
Finally, participants will to apply checkers to their own code, to
begin writing their own checkers, or to refine existing ones. They
will work in small groups, both to permit the presenters to spend
enough time with each group and also to permit participants to learn
from one another.
