Search the Dagstuhl Website
Looking for information on the websites of the individual seminars? - Then please:
Not found what you are looking for? - Some of our services have separate websites, each with its own search option. Please check the following list:
Schloss Dagstuhl - LZI - Logo
Schloss Dagstuhl Services
Within this website:
External resources:
  • DOOR (for registering your stay at Dagstuhl)
  • DOSA (for proposing future Dagstuhl Seminars or Dagstuhl Perspectives Workshops)
Within this website:
External resources:
Within this website:
External resources:
  • the dblp Computer Science Bibliography

Dagstuhl Seminar 01411

Proof Theory in Computer Science

( Oct 07 – Oct 12, 2001 )

(Click in the middle of the image to enlarge)

Please use the following short url to reference this page:



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.

  • Sergei N. Artemov (Cornell University, US)
  • Jeremy Avigad (Carnegie Mellon University, US) [dblp]
  • Arnold Beckmann (TU Wien, AT) [dblp]
  • Lev D. Beklemishev (Utrecht University, NL) [dblp]
  • Ulrich Berger (Swansea University, GB) [dblp]
  • Thierry Coquand (Chalmers - Göteborg, SE) [dblp]
  • Kosta Dosen (Serbian Academy of Sciences and Arts, YU)
  • Wlodzimierz Drabent (Polish Academy of Sciences - Warsaw, PL)
  • Roy Dyckhoff (University of St. Andrews, GB)
  • Birgit Elbl (Universität der Bundeswehr - München, DE)
  • Christian G. Fermüller (TU Wien, AT)
  • Lev Gordeev (Universität Tübingen, DE) [dblp]
  • J. Roger Hindley (University of Wales - Swansea, GB)
  • Gerhard Jäger (Universität Bern, CH)
  • Jan Johannsen (LMU München, DE) [dblp]
  • Reinhard Kahle (University of Coimbra, PT)
  • Oliver Kullmann (Swansea University, GB) [dblp]
  • Hans Leiß (LMU München, DE)
  • Alexander Leitsch (TU Wien, AT) [dblp]
  • Ralph Matthes (LMU München, DE)
  • Yiannis Moschovakis (UCLA, US) [dblp]
  • Stanislas Nanchen (ETH Zürich, CH)
  • Isabel Oitavem (Universidade Nova de Lisboa, PT)
  • Geoffrey Ostrin (Universität Bern, CH)
  • Peter H. Schmitt (KIT - Karlsruher Institut für Technologie, DE) [dblp]
  • Peter Schroeder-Heister (Universität Tübingen, DE)
  • Helmut Schwichtenberg (LMU München, DE) [dblp]
  • Anton Setzer (Swansea University, GB)
  • Robert Stärk (ETH Zürich, CH)
  • Jaco van de Pol (CWI - Amsterdam, NL) [dblp]
  • Andreas Weiermann (Universität Münster, DE) [dblp]