Types for Tools: Applications of Type Theoretic Techniques

Motivation

Type systems have proven to be the most cost-effective technique for ensuring software systems safety to have gained widespread acceptance. Over the last thirty years, a variety of type systems have been deployed and adopted in programming languages such as Haskell, Java and C#. Types and type systems were originally intended to characterize program properties amenable to mechanical checking for the purpose of preventing certain kinds of run-time errors. In recent years, type-theoretic techniques have been successfully applied to address software engineering challenges and used in software engineering tools that automate tasks related to the maintenance, improvement, translation, restructuring, and upgrading of existing software. These applications are becoming increasingly subtle and application domain specific. Examples of such novel applications of type-theoretic principles include:

• Type inference and type-directed transformation have been used in the translation of large COBOL application for Y2K compliance.
• Linear types have been used to enforce protocols present in the interface between the Windows 2000 kernel and its device drivers.
• Parametric type polymorphism has been retrofitted onto main stream programming languages in a provably sound manner.
• Type constraints have been used as the basis for automating code refactorings related to type generalization.
• Type systems are being used to define the well-formedness of XML documents, with safety guarantees for the input and output of such documents.
• Ownership types which capture the dynamic topology of object graphs have been proposed as a mechanism for enforcing locality in software upgrades of object-oriented databases.
• Behavioral types as automatically checked stateful interface specifications for distributed components such as web services.
• Type for region-based memory management, support for both automatic inference of regions and, for profiling-driven engineering by programmers

These examples all share the important characteristic that type theoretical ideas have been applied to solve software engineering problems and that the application has been embodied in a practical tool. Although there is a growing number of such applications, the types community, the software engineering community, and the tools development community are still largely distinct, with their own set of conferences and meetings.

This workshop brings together the technical leaders of these communities. The participants, between 30 and 40 researchers, will be selected to cover the fields of type theory, static program analysis, and applied software engineering. The workshhop will consist of a combination of longer tutorial-style talks (1.5 hours) and a collection of short 20 minutes research presentations. Significant time is planned for informal and group discussion of selected topics.