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.
- Thorsten Altenkirch (University of Nottingham, GB)
- David R. Aspinall (University of Edinburgh, GB)
- Lennart Augustsson (Chalmers UT - Göteborg, SE) [dblp]
- Gilles Barthe (INRIA Sophia Antipolis - Méditerranée, FR) [dblp]
- Magnus Carlsson (Göteborg, SE)
- Thierry Coquand (Chalmers - Göteborg, SE) [dblp]
- Peter Dybjer (Chalmers - Göteborg, SE)
- Amy Felty (University of Ottawa, CA) [dblp]
- Andrzej Filinski (University of Copenhagen, DK) [dblp]
- Daniel Fridlender (Universidad Nacional de Córdoba, AR)
- Jacques Garrigue (Kyoto University, JP)
- Douglas J. Howe (Carleton University - Ottawa, CA)
- Yorck Hünke (University of Oxford, GB)
- Johan Jeuring (Utrecht University, NL) [dblp]
- Christoph Kreitz (Cornell University, US)
- Zhaohui Luo (Durham University, GB)
- Michel Mauny (INRIA - Le Chesnay, FR)
- Conor McBride (Durham University, GB) [dblp]
- Eugenio Moggi (University of Genova, IT)
- Matthias Neubauer (Universität Freiburg, DE)
- Christine Paulin-Möhring (Université Paris Sud, FR) [dblp]
- Randy Pollack (University of Edinburgh, GB)
- Didier Remy (INRIA - Le Chesnay, FR) [dblp]
- Anton Setzer (Swansea University, GB)
- Zhong Shao (Yale University, US) [dblp]
- Tim Sheard (Oregon Health & Science University - Beaverton, US)
- Walid Taha (Rice University - Houston, US) [dblp]
- Peter Thiemann (Universität Freiburg, DE) [dblp]
- Joe Wells (Heriot-Watt University Edinburgh, GB)
- Kwong-Cheong Wong (INRIA Sophia Antipolis - Méditerranée, FR)
- Christoph Zenger (TU München, DE)