19. – 24. Juni 2005, Dagstuhl-Seminar 05251

Types for Tools: Applications of Type Theoretic Techniques


Fritz Henglein (University of Copenhagen, DK)
Martin Odersky (EPFL – Lausanne, CH)
Frank Tip (IBM TJ Watson Research Center – Hawthorne, US)
Jan Vitek (Purdue University – West Lafayette, US)

Auskunft zu diesem Dagstuhl-Seminar erteilt

Dagstuhl Service Team




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.


In der Reihe Dagstuhl Reports werden alle Dagstuhl-Seminare und Dagstuhl-Perspektiven-Workshops dokumentiert. Die Organisatoren stellen zusammen mit dem Collector des Seminars einen Bericht zusammen, der die Beiträge der Autoren zusammenfasst und um eine Zusammenfassung ergänzt.


Download Übersichtsflyer (PDF).

Dagstuhl's Impact

Bitte informieren Sie uns, wenn eine Veröffentlichung ausgehend von Ihrem Seminar entsteht. Derartige Veröffentlichungen werden von uns in der Rubrik Dagstuhl's Impact separat aufgelistet  und im Erdgeschoss der Bibliothek präsentiert.


Es besteht weiterhin die Möglichkeit, eine umfassende Kollektion begutachteter Arbeiten in der Reihe Dagstuhl Follow-Ups zu publizieren.