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

Contact

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.