Publications in 2011

Layer Systems for Proving Confluence
Bertram Felgenhauer, Harald Zankl, and Aart Middeldorp
Proceedings of the 30th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011), Leibniz International Proceedings in Informatics 13, pp. 288 – 299, 2011.

Generalized and Formalized Uncurrying
Christian Sternagel and René Thiemann
Proceedings of the 8th International Symposium on Frontiers of Combining Systems (FroCoS 2011), Lecture Notes in Artificial Intelligence 6989, pp. 243 – 258, 2011.

The Exact Hardness of Deciding Derivational and Runtime Complexity
Andreas Schnabl and Jakob Grue Simonsen
Proceedings of the 25th International Workshop on Computer Science Logic / 20th Annual Conference of the EACSL (CSL 2011), Leibniz International Proceedings in Informatics 12, pp. 481 – 495, 2011.

Decreasing Diagrams and Relative Termination
Nao Hirokawa and Aart Middeldorp
Journal of Automated Reasoning 47(4), pp. 481 – 501, 2011.

Termination of Isabelle Functions via Termination of Rewriting
Alexander Krauss, Christian Sternagel, René Thiemann, Carsten Fuhs, and Jürgen Giesl
Proceedings of the 2nd International Conference on Interactive Theorem Proving (ITP 2011), Lecture Notes in Computer Science 6898, pp. 152 – 167, 2011.

CSI – A Confluence Tool
Harald Zankl, Bertram Felgenhauer, and Aart Middeldorp
Proceedings of the 23rd International Conference on Automated Deduction (CADE 2011), Lecture Notes in Artificial Intelligence 6803, pp. 499 – 505, 2011.

AC Completion with Termination Tools
Sarah Winkler and Aart Middeldorp
Proceedings of the 23rd International Conference on Automated Deduction (CADE 2011), Lecture Notes in Artificial Intelligence 6803, pp. 492 – 498, 2011.

On Transfinite Knuth-Bendix Orders
Laura Kovács, Georg Moser, and Andrei Voronkov
Proceedings of the 23rd International Conference on Automated Deduction (CADE 2011), Lecture Notes in Artificial Intelligence 6803, pp. 384 – 399, 2011.

The Derivational Complexity Induced by the Dependency Pair Method
Georg Moser and Andreas Schnabl
Logical Methods in Computer Science 7(3:1), pp. 1 – 38, 2011.

Joint Spectral Radius Theory for Automated Complexity Analysis of Rewrite Systems
Aart Middeldorp, Georg Moser, Friedrich Neurauter, Johannes Waldmann, and Harald Zankl
Proceedings of the 4th International Conference on Algebraic Informatics (CAI 2011), Lecture Notes in Computer Science 6742, pp. 1 – 20, 2011.

Labelings for Decreasing Diagrams
Harald Zankl, Bertram Felgenhauer, and Aart Middeldorp
Proceedings of the 22nd International Conference on Rewriting Techniques and Applications (RTA 2011), Leibniz International Proceedings in Informatics 10, pp. 377 – 392, 2011.

Modular and Certified Semantic Labeling and Unlabeling
Christian Sternagel and René Thiemann
Proceedings of the 22nd International Conference on Rewriting Techniques and Applications (RTA 2011), Leibniz International Proceedings in Informatics 10, pp. 329 – 344, 2011.

Revisiting Matrix Interpretations for Proving Termination of Term Rewriting
Friedrich Neurauter and Aart Middeldorp
Proceedings of the 22nd International Conference on Rewriting Techniques and Applications (RTA 2011), Leibniz International Proceedings in Informatics 10, pp. 251 – 266, 2011.

Termination Proofs in the Dependency Pair Framework May Induce Multiple Recursive Derivational Complexity
Georg Moser and Andreas Schnabl
Proceedings of the 22nd International Conference on Rewriting Techniques and Applications (RTA 2011), Leibniz International Proceedings in Informatics 10, pp. 235 – 250, 2011.

A Path Order for Rewrite Systems that Compute Exponential Time Functions
Martin Avanzini, Naohi Eguchi, and Georg Moser
Proceedings of the 22nd International Conference on Rewriting Techniques and Applications (RTA 2011), Leibniz International Proceedings in Informatics 10, pp. 123 – 138, 2011.

Executable Transitive Closures of Finite Relations
Christian Sternagel and René Thiemann
The Archive of Formal Proofs, 2011.

Uncurrying for Innermost Termination and Derivational Complexity
Harald Zankl, Nao Hirokawa, and Aart Middeldorp
Proceedings of the 5th International Workshop on Higher-Order Rewriting (HOR 2010), Electronic Proceedings in Theoretical Computer Science 49, pp. 46 – 57, 2011.

Automated Termination Proofs for Haskell by Term Rewriting
Jürgen Giesl, Matthias Raffelsieper, Peter Schneider-Kamp, Stephan Swiderski, and René Thiemann
ACM Transactions on Programming Languages and Systems 33(2), 2011.