Developing and Using Pluggable Type Systems

*
Accepted Session
Long Form
Intermediate
Scheduled: Tuesday, June 26, 2012 from 10:00 – 11:45am in B204

Excerpt

A pluggable type system extends a language's built-in type system to
confer additional compile-time guarantees. We will explain the theory and
practice of pluggable types.

Description

A pluggable type system extends a language’s built-in type system to
confer additional compile-time guarantees. We will explain the theory and
practice of pluggable types. The material is relevant for anyone who wishes
to increase confidence in their code.
After this session, you will have the knowledge to:

  • analyze a problem to determine whether pluggable type-checking is
    appropriate;
  • design a domain-specific type system; implement a simple
    type-checker (in as little as 4 lines of code!);
  • scale a simple type-checker to more sophisticated properties;
  • and better appreciate both object-oriented types and flexible
    verification techniques.

While the theory is general, our hands-on exercises will use a
state-of-the-art system, the Checker Framework, that works for the Java
language, scales to millions of lines of code, and is being adopted in the
research and industrial communities. Such a framework enables researchers
to easily evaluate their type systems in the context of a widely-used
industrial language, Java. It enables non-researchers to verify their
code in a lightweight way and to create custom analyses. And it enables
students to better appreciate type system concepts.

We will:

  • guide the audience through installing the Checker Framework,
    including how to set up Eclipse integration;
  • teach how to use some of the checkers included with the Checker
    Framework;
  • discuss other types of errors that one would like to be prevented at
    compile time;
  • and teach how to write a new type checker to prevent the errors we
    come up with in our discussion.

Audience participation is desired! We encourage the audience to come
prepared with a laptop with a working Java environment (Eclipse
optional).
Additional material is available here.

Speaking experience

Open Source Bridge 2011, ~15 participants
http://opensourcebridge.org/sessions/658

OOPSLA 2009, ~15 participants
http://www.oopsla.org/oopsla2009/program/tutorials/171-detecting-and-preventing-bugs-with-pluggable-type-checking

We have been accepted to present a similar tutorial at
the O'Reilly OSCON 2012 convention this upcoming July.

Speakers