Proof theory is one of the central pillars of mathematical logic. In
the early 20th century, Hilbert's programme proposed to establish the
consistency of mathematics by finitary means. Proof-theoretic
investigations in this tradition were largely concerned with questions
of

In structural proof theory we can distinguish two traditions. The first, with mathematical roots, is concerned with first-order logic, and encompasses such methods as Herbrand's theorem, Hilbert's epsilon-calculus or Gödel's Dialectica interpretation. The other tradition derives its motivations from computer science, therefore coming later than the first tradition, and is concerned with the propositional structure of proofs. It uses methods such as the Curry-Howard isomorphism, algebraic semantics, linear logic, proof nets and deep inference. The French project partners are situated primarily in the latter tradition, and the Austrian project partners in the former tradition. The proposed project will thus play an important role in the cross-fertilization of these different subfields of structural proof theory.

In both traditions, analytic proofs and procedures for obtaining such
proofs play a paramount role. The aim of the proposed project is to
further deepen the understanding of the structural properties of
analytic proofs. More specifically, we plan to investigate extensions
of the classical notion of

Structural proof theory plays a crucial role in the foundations of
programming language.
At the

The present project is, from the French side, a prolongation of the ANR INFER project "Theory and Application of Deep Inference" between LIX (Palaiseau), LORIA (Nancy), and PPS (Paris). INFER has provided the theoretical basis on deep inference that is needed for our proposed research in STRUCTURAL.

The collaboration between the Austrian and French teams has been preceded by two ÖAD/PHC exchange projects, which have precisely the aim of initiating collaborations: the ÖAD-PHC Amadeus project "Logic-Based Analysis of Computation" FR 10/2009 between PPS and Universität Innsbruck, and the ÖAD-PHC Amadeus on "The Realm of Cut Elimination" between LIX, PPS, and TU Wien (Austria).

Preuves, Programmes, Systèmes
(PPS)

Responsible: Michel Parigot

Laboratoire d'Informatique d'Ecole Polytechnique (LIX)

Responsible: Lutz Straßburger

Universität Innsbruck

Responsible: Georg Moser

TU Vienna

Responsible: Matthias Baaz

Responsible: Michel Parigot

Laboratoire d'Informatique d'Ecole Polytechnique (LIX)

Responsible: Lutz Straßburger

Universität Innsbruck

Responsible: Georg Moser

TU Vienna

Responsible: Matthias Baaz

There is an open 12-month postdoc
position at LIX financed by
the ANR within
this project.

Applicants must have a Ph.D. or equivalent in computer science or
mathematics, and should have a strong background in proof theory and/or
related topics.

Applications should be sent via email to Lutz
Straßburger and should include a CV, a short research statement (1-2
pages), and one or two recommendation letters.

Deadline: January 31, 2013

Last update: January 10, 2013 Lutz Straßburger