October 7 – 12 , 2001, Dagstuhl Seminar 01411

Proof Theory in Computer Science


Reinhard Kahle (University of Coimbra, PT)
Peter Schroeder-Heister (Universität Tübingen, DE)
Robert Stärk (ETH Zürich, CH)

For support, please contact

Dagstuhl Service Team


External Homepage
List of Participants
Dagstuhl's Impact: Documents available
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.


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

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.


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