Dagstuhl Seminar 05251
Types for Tools: Applications of Type Theoretic Techniques
( Jun 19 – Jun 24, 2005 )
- 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)
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.
- Uwe Aßmann (TU Dresden, DE) [dblp]
- Rastislav Bodik (University of California - Berkeley, US) [dblp]
- John T. Boyland (Univ. Wisconsin - Milwaukee, US)
- Brian Demsky (MIT - Cambridge, US) [dblp]
- Sophia Drossopoulou (Imperial College London, GB) [dblp]
- Manuel A. Fähndrich (Microsoft Research - Redmond, US) [dblp]
- Cormac Flanagan (University of California - Santa Cruz, US) [dblp]
- Robert Fuhrer (IBM TJ Watson Research Center - Hawthorne, US)
- John Hatcliff (Kansas State University, US) [dblp]
- Görel Hedin (Lund University, SE) [dblp]
- Fritz Henglein (University of Copenhagen, DK) [dblp]
- Martin Hofmann (LMU München, DE) [dblp]
- Atsushi Igarashi (Kyoto University, JP) [dblp]
- Suresh Jagannathan (Purdue University - West Lafayette, US) [dblp]
- Jaakko Järvi (Texas A&M University - College Station, US)
- Adam Kiezun (MIT - Cambridge, US)
- Shriram Krishnamurthi (Brown University - Providence, US) [dblp]
- Julia Lawall (University of Copenhagen, DK) [dblp]
- Anne-Francoise Le Meur (University of Lille I, FR)
- Gary T. Leavens (Iowa State University, US) [dblp]
- Todd Millstein (UCLA, US) [dblp]
- Anders Møller (Aarhus University, DK) [dblp]
- Oscar M. Nierstrasz (Universität Bern, CH) [dblp]
- James Noble (University of Wellington, NZ) [dblp]
- Martin Odersky (EPFL - Lausanne, CH) [dblp]
- Arnd Poetzsch-Heffter (TU Kaiserslautern, DE) [dblp]
- Francois Pottier (INRIA - Le Chesnay, FR) [dblp]
- Mukund Raghavachari (IBM TJ Watson Research Center - Yorktown Heights, US)
- Jakob Rehof (Microsoft Research - Redmond, US) [dblp]
- Noam Rinetzky (Tel Aviv University, IL) [dblp]
- Barbara G. Ryder (Rutgers University - Piscataway, US) [dblp]
- Jan Schäfer (TU Kaiserslautern, DE)
- Peter Sewell (University of Cambridge, GB) [dblp]
- Gregor Snelting (Universität Passau, DE) [dblp]
- Peter Thiemann (Universität Freiburg, DE) [dblp]
- Frank Tip (IBM TJ Watson Research Center - Hawthorne, US) [dblp]
- Mandana Vaziri (IBM TJ Watson Research Center - Yorktown Heights, US) [dblp]
- Jan Vitek (Purdue University - West Lafayette, US) [dblp]
- Christoph von Praun (IBM TJ Watson Research Center - Yorktown Heights, US) [dblp]
- David Walker (Princeton University, US) [dblp]