07. – 12. Oktober 2001, Dagstuhl Seminar 01411

Proof Theory in Computer Science


R. Kahle (Tübingen), P. Schröder-Heister (Tübingen), R. Stärk (Zürich)

Auskunft zu diesem Dagstuhl Seminar erteilt

Dagstuhl Service Team


Dagstuhl's Impact: Dokumente verfügbar
Externe Homepage
Dagstuhl-Seminar-Report 322

Proof theory has long been established as a basic discipline of mathematical logic. In recent years it has become increasingly relevant to computer science. The deductive apparatus provided by proof theory has proved to be useful both for metatheoretical purposes and for practical applications in various fields of computer science.

The aim of this conference is to assess which role proof theory is already playing in computer science, and which role it might play in further developments. Is proof theory going to be the most preferential approach to the logical foundations of computer science? Does is provide viable alternatives in areas where model-theoretic approaches are predominant?

A central focus of the conference may be captured by the slogan "logics for programs", i.e. the proof theoretic approach in dealing with design, development and application of programming languages.

Examples of main topics are:

  • Applicative and type theories in functional programming
  • Extensions of logic programming with higher type concepts
  • Computational complexity and term rewriting from a proof-theoretic point of view
  • Automated and interactive procedures in proof search
  • The use of special formal systems (e.g. substructural logics) in the specification and verification of programs.

This list is by no means exhaustive. Any contribution is welcome which promises to shed some light on the topic of the conference.

Proof theory is not a uniform subject at all. The list of invited participants includes researchers from different research paradigms. In particular, we are inviting both proof theorists in the more traditional "theoretical" or "mathematical" sense, and computer scientists using proof theoretic tools in the area of deduction. We hope that novel and promising ideas evolve by bringing such people together.

It is planned to publish a proceedings volume in the Springer LNCS series. Participants who are willing to contribute to this volume are invited to submit a manuscript by April 2001. Further details (format and length of paper, deadlines, program committee etc.) will be published soon.

However, it should be emphasized that submission and / or acceptance of a manuscript is no precondition for a presentation at the conference.


Bücher der Teilnehmer 

Buchausstellung im Erdgeschoss der Bibliothek

(nur in der Veranstaltungswoche).


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


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.