### Structural and Computational Proof Theory

This is a joint project between Austria and France represented by the following institutions:

- University of Innsbruck
- Vienna University of Technology
- Université Paris Diderot
- INRIA Saclay — Ile-de-France

The project is about bringing together different aspects and developments in structural proof theory, namely deep inference, the Curry-Howard correspondence, term rewriting, and Hilbert’s epsilon calculus.

#### Members

The project is coordinated by

- Georg Moser (coordinator Austria)
- Matthias Baaz
- Michel Parigot (coordinator France)
- Lutz Straßburger

The node Innsbruck consists of

- Martin Avanzini
- Georg Moser
- Stéphane Gimenez
- Michael Schaper

#### Meetings

- Kick-Off Workshop STRUCTURAL, June 15—17, 2011, Paris
- Workshop STRUCTURAL, 2nd meeting, October 26 – 28, 2011, Innsbruck
- Collegium Logicum 2012: Structural Proof Theory

- LIX Colloquium 2013, held from November 5—7 in Palaiseau

Project related publications from Innsbruck can be found below. For publications of the Vienna node, kindly see the website of the Computational Logic group at the Vienna University of Technology.

Further information on the project, in particular on the French project partners can be found at the STRUCTURAL page at LIX.

#### FWF “Joint Project” project number

I-603 N18#### Contact

georg moser at uibk dot ac dot at#### Publications

KBOs, Ordinals, Subrecursive Hierarchies and All That

Georg Moser

Journal of Logic and Computation Advanced Access,
2014.

A New Order-Theoretic Characterisation of the Polytime Computable Functions

Martin Avanzini, Naohi Eguchi, and Georg Moser

Theoretical Computer Science 585,
pp. 3 – 24,
2015.

Verifying Polytime Computability Automatically

Martin Avanzini

PhD thesis, University of Innsbruck, 2013.

Polynomial Path Orders

Martin Avanzini and Georg Moser

Logical Methods in Computer Science 9(4),
pp. 1 – 42,
2013.

The Structure of Interaction

Stéphane Gimenez and Georg Moser

Proceedings of the 27th International Workshop on Computer Science Logic / 22nd Annual Conference of the EACSL (CSL 2013),
Leibniz International Proceedings in Informatics 23,
pp. 316 – 331,
2013.

A Haskell Library for Term Rewriting

Bertram Felgenhauer, Martin Avanzini, and Christian Sternagel

Proceedings of the 1st International Workshop on Haskell and Rewriting Techniques (HART 2013),
2013.

Tyrolean Complexity Tool: Features and Usage

Martin Avanzini and Georg Moser

Proceedings of the 24th International Conference on Rewriting Techniques and Applications (RTA 2013),
Leibniz International Proceedings in Informatics 21,
pp. 71 – 80,
2013.

A Combination Framework for Complexity

Martin Avanzini and Georg Moser

Proceedings of the 24th International Conference on Rewriting Techniques and Applications (RTA 2013),
Leibniz International Proceedings in Informatics 21,
pp. 55 – 70,
2013.

New Order-theoretic Characterisation of the Polytime Computable Functions

Martin Avanzini, Naohi Eguchi, and Georg Moser

Proceedings of the 10th Asian Symposium on Programming Languages and Systems (APLAS 2012),
Lecture Notes in Computer Science 7705,
pp. 280 – 295,
2012.

Termination Graphs Revisited

Georg Moser and Michael Schaper

Proceedings of the 12th International Workshop on Termination (WST 2012),
pp. 64 – 68,
2012.