Dependent Type Theory meets Practical Programming

Modern programming languagees rely on advanced type systems that detect errors at compile-time. While the benefits of type systems have long been recognized, there are some areas where the standard systems in programming languages are not expressive enough. Language designers usually trade expressiveness for decidability of the type system. Some interesting programs will always be rejected (despite their semantical soundness) or be assigned uninformative types.

There are several remedies to this situation. We argue that dependent type systems, which allow the formation of types that explicitly depend on other types or values, are one of the most promising approaches. These systems are well-investigated from a theoretical point of view by logicians and type theorists. For example, dependent types are used in proof assistants to implement various logics and there are sophisticated proof editors for developing programs in a dependently typed language.

To the present day, the impact of these developments on practical programming has been small, partially because of the level of sophistication of these systems and of their type checkers. Only recently, there have been efforts to integrate dependent systems into intermediate languages in compilers, for example, the TAL compiler (Morrisett and others http://www.cs.cornell.edu/home/jgm/), and actual programming languages, for example, Cayenne (Augustsson http://www.cs.chalmers.se/~augustss/) and DML (Xi and Pfenning http://www.ececs.uc.edu/~hwxi/). Additional uses have been identified in high-profile applications such as mobile code security. For example, proof carrying code (Necula and Lee http://www-nt.cs.berkeley.edu/home/necula/public_html/) relies on a dependently typed lambda calculus to encode proof terms.

Now the time is ripe to bring together researchers from the two communities (type theorists and programming experts), and to further cross-fertilization of ideas, techniques and formalisms developed independently in these communities. In particular, the seminar shall make researchers in programming languages aware of new developments and research directions on the theory side; point out to theorists practical uses of advanced type systems and urge them to address theoretical problems arising in emerging applications.

The need for such a seminar became clear during the first international Workshop on Dependent Types in Programming (http://www.md.chalmers.se/Cs/Research/Semantics/APPSEM/dtp99.html), held in G6teborg in March 1999. A second international Workshop on Dependent Types in Programming (http://www-sop.inria.fr/oasis/DTP00/index.html) has been held in Ponte de Lima in July 2000, but it is hard to discuss the problems pointed out above in a one-day workshop.