Structural and Computational Proof Theory


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

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

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@uibk.ac.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.
Nach oben scrollen