http://www.dagstuhl.de/01341

19. – 24. August 2001, Dagstuhl Seminar 01341

Dependent Type Theory meets Practical Programming

Organisatoren

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

Auskunft zu diesem Dagstuhl Seminar erteilt

Dagstuhl Service Team

Dokumente

Teilnehmerliste
Dagstuhl's Impact: Dokumente verfügbar
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.

Buchausstellung

Bücher der Teilnehmer 

Buchausstellung im Erdgeschoss der Bibliothek

(nur in der Veranstaltungswoche).

Dokumentation

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).

Publikationen

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

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.