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