https://www.dagstuhl.de/01341

August 19 – 24 , 2001, Dagstuhl Seminar 01341

Dependent Type Theory meets Practical Programming

Organizers

Gilles Barthe (INRIA Sophia Antipolis – Méditerranée, FR)
Peter Dybjer (Chalmers – Göteborg, SE)
Peter Thiemann (Universität Freiburg, DE)

For support, please contact

Dagstuhl Service Team

Documents

List of Participants
Dagstuhl's Impact: Documents available
Dagstuhl-Seminar-Report 317

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.

Documentation

In the series Dagstuhl Reports each Dagstuhl Seminar and Dagstuhl Perspectives Workshop is documented. The seminar organizers, in cooperation with the collector, prepare a report that includes contributions from the participants' talks together with a summary of the seminar.

 

Download overview leaflet (PDF).

Publications

Furthermore, a comprehensive peer-reviewed collection of research papers can be published in the series Dagstuhl Follow-Ups.

Dagstuhl's Impact

Please inform us when a publication was published as a result from your seminar. These publications are listed in the category Dagstuhl's Impact and are presented on a special shelf on the ground floor of the library.