Proof Theory, Computation, Complexity

International workshop

July 3rd and 4th, 2003, Dresden

Aims and Scope

The workshop PCC '03 is held in conjunction with the Summer School on Proof Theory, Computation, and Complexity in Dresden, joining the successors to last year's corresponding events (Proof Theory and Computation in Dresden and Proof, Computation, Complexity in Tübingen). The aim of PCC is to stimulate research in proof theory, computation, and complexity, focusing on issues which combine logical and computational aspects. Topics may include applications of formal inference systems in computer science, as well as new developments in proof theory motivated by computer science demands. Specific areas of interest are (non-exhaustively listed) foundations for declarative programming languages, logical methods in specification and program development, new developments in structural proof theory, and implicit computational complexity.


PCC is intended to be a lively forum for presenting and discussing recent work. There will be no published proceedings of full papers, allowing for simultaneous or subsequent conference or journal submission of the presented material, but participants who want to contribute a talk are asked to submit a one-page-abstract (LaTeX). The collection of abstracts will be available at the meeting.

Deadline: May 25th, 2003
Submission of abstracts:

Registration and further information


Preliminary Program

Thursday, July 3rd

9:30 Morning Session

Kai Brünnler Interpolation as Symmetric Cut Elimination
Alwen Tiu Induction and Coinduction in Sequent Calculus
Coffee Break
Phiniki StouppaIs deep inference necessary for good proof theoretic treatments of modal logic?
Lutz StraßburgerSystem NEL is undecidable

14:15 Afternoon Session

Pascal HitzlerDomain Theory and Nonmonotonic Reasoning
Birgit ElblGoal Composition and Local Variables

Excursion & Workshop Dinner

Friday, July 4th

9:30 Morning Session

Karl-Heinz NigglThe Garland Measure and Computational Complexity of Imperative Programs
Henning WunderlichCharacterising FPTIME Through Stack Programs with Arbitrary Primitives
Coffee Break
Isabel OitavemCharacterising PSPACE with Pointers
Lars KristiansenComputing without the Successor Function. New Characterizations of Well Known Complexity Classes.

14:00 Afternoon Session

Heinrich WansingOn the Negation of Action Types: Constructive Concurrent PDL
Coffee Break
Monika SeisenbergerA-Translation of Higman's Lemma
Reinhard KahleDynamic Logic Programming