Institute of Computer Science
University of Innsbruck
Home Research Teaching Members Events News
Research
publications projects software
publications
2012 2011 2010 2009 2008 2007 2006 2005 2004

All Publications

Ordinals and Knuth-Bendix Orders
Sarah Winkler, Harald Zankl, and Aart Middeldorp
Proceedings of the 18th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-18), Lecture Notes in Artificial Intelligence (Advanced Research in Computing and Software Science) 7180, pp. 420 – 434, 2012.

On the Domain and Dimension Hierarchy of Matrix Interpretations
Friedrich Neurauter and Aart Middeldorp
Proceedings of the 18th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-18), Lecture Notes in Artificial Intelligence (Advanced Research in Computing and Software Science) 7180, pp. 320 – 334, 2012.

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.

Loops under Strategies … Continued
René Thiemann, Christian Sternagel, Jürgen Giesl, and Peter Schneider-Kamp
Proceedings of the 1st International Workshop on Strategies in Rewriting, Proving, and Programming (IWS 2010), Electronic Proceedings in Theoretical Computer Science 44, pp. 51 – 65, 2010.

Automatic Certification of Termination Proofs
Christian Sternagel
PhD thesis, University of Innsbruck, 2010.

Termination Analysis by Tree Automata Completion
Martin Korp
PhD thesis, University of Innsbruck, 2010.

Revisiting Matrix Interpretations for Polynomial Derivational Complexity of Term Rewriting
Friedrich Neurauter, Harald Zankl, and Aart Middeldorp
Proceedings of the 17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-17), Lecture Notes in Computer Science (Advanced Research in Computing and Software Science) 6397, pp. 550 – 564, 2010.

Signature Extensions Preserve Termination – An Alternative Proof via Dependency Pairs
Christian Sternagel and René Thiemann
Proceedings of the 19th Annual Conference of the European Association for Computer Science Logic (CSL 2010), Lecture Notes in Computer Science 6247, pp. 514 – 528, 2010.

Executable Multivariate Polynomials
Christian Sternagel and René Thiemann
The Archive of Formal Proofs, 2010.

POP* and Semantic Labeling using SAT
Martin Avanzini
Interfaces: Explorations in Logic, Language and Computation, Lecture Notes in Artificial Intelligence 6211, pp. 155 – 166, 2010.

Cdiprover3: A Tool for Proving Derivational Complexities of Term Rewriting Systems
Andreas Schnabl
Interfaces: Explorations in Logic, Language and Computation, Lecture Notes in Artificial Intelligence 6211, pp. 142 – 154, 2010.

Termination Tools in Ordered Completion
Sarah Winkler and Aart Middeldorp
Proceedings of the 5th International Joint Conference on Automated Reasoning (IJCAR 2010), Lecture Notes in Artificial Intelligence 6173, pp. 518 – 532, 2010.

Monotonicity Criteria for Polynomial Interpretations over the Naturals
Friedrich Neurauter, Harald Zankl, and Aart Middeldorp
Proceedings of the 5th International Joint Conference on Automated Reasoning (IJCAR 2010), Lecture Notes in Artificial Intelligence 6173, pp. 502 – 517, 2010.

Decreasing Diagrams and Relative Termination
Nao Hirokawa and Aart Middeldorp
Proceedings of the 5th International Joint Conference on Automated Reasoning (IJCAR 2010), Lecture Notes in Artificial Intelligence 6173, pp. 487 – 501, 2010.

Executable Matrix Operations on Matrices of Arbitrary Dimensions
Christian Sternagel and René Thiemann
The Archive of Formal Proofs, 2010.

Abstract Rewriting
Christian Sternagel and René Thiemann
The Archive of Formal Proofs, 2010.

Optimizing mkbTT (System Description)
Sarah Winkler, Haruhiko Sato, Aart Middeldorp, and Masahito Kurihara
Proceedings of the 21st International Conference on Rewriting Techniques and Applications (RTA 2010), Leibniz International Proceedings in Informatics 6, pp. 373 – 384, 2010.

Modular Complexity Analysis via Relative Complexity
Harald Zankl and Martin Korp
Proceedings of the 21st International Conference on Rewriting Techniques and Applications (RTA 2010), Leibniz International Proceedings in Informatics 6, pp. 385 – 400, 2010.

Certified Subterm Criterion and Certified Usable Rules
Christian Sternagel and René Thiemann
Proceedings of the 21st International Conference on Rewriting Techniques and Applications (RTA 2010), Leibniz International Proceedings in Informatics 6, pp. 325 – 340, 2010.

Polynomial Interpretations over the Reals do not Subsume Polynomial Interpretations over the Integers
Friedrich Neurauter and Aart Middeldorp
Proceedings of the 21st International Conference on Rewriting Techniques and Applications (RTA 2010), Leibniz International Proceedings in Informatics 6, pp. 243 – 258, 2010.

Closing the Gap Between Runtime Complexity and Polytime Complexity
Martin Avanzini and Georg Moser
Proceedings of the 21st International Conference on Rewriting Techniques and Applications (RTA 2010), Leibniz International Proceedings in Informatics 6, pp. 33 – 48, 2010.

Satisfiability of Non-Linear (Ir)rational Arithmetic
Harald Zankl and Aart Middeldorp
Proceedings of the 16th International Conference on Logic for Programming and Automated Reasoning (LPAR-16), Lecture Notes in Artificial Intelligence 6355, pp. 481 – 500, 2010.

Complexity Analysis by Graph Rewriting
Martin Avanzini and Georg Moser
Proceedings of the 10th International Symposium on Functional and Logic Programming (FLOPS 2010), Lecture Notes in Computer Science 6009, pp. 257 – 271, 2010.

Finding and Certifying Loops
Harald Zankl, Christian Sternagel, Dieter Hofbauer, and Aart Middeldorp
Proceedings of the 36th International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM 2010), Lecture Notes in Computer Science 5901, pp. 755 – 766, 2010.

Lazy Termination Analysis
Harald Zankl
PhD thesis, University of Innsbruck, 2009.

Increasing interpretations
Harald Zankl and Aart Middeldorp
Annals of Mathematics and Artificial Intelligence 56(1), pp. 87 – 108, 2009.

Match-Bounds Revisited
Martin Korp and Aart Middeldorp
Information and Computation 207(11), pp. 1259 – 1283, 2009.

Automated Termination Proofs for Logic Programs by Term Rewriting
Peter Schneider-Kamp, Jürgen Giesl, Alexander Serebrenik, and René Thiemann
ACM Transactions on Computational Logic 11(1), pp. 1 – 52, 2009.

Proof Theory at Work: Complexity Analysis of Term Rewrite Systems
Georg Moser
Habilitation thesis, University of Innsbruck,  2009.

Certification of Termination Proofs using CeTA
René Thiemann and Christian Sternagel
Proceedings of the 22nd International Conference on Theorem Proving in Higher-Order Logics (TPHOLs 2009), Lecture Notes in Computer Science 5674, pp. 452 – 468, 2009.

Transforming SAT into Termination of Rewriting
Harald Zankl, Christian Sternagel, and Aart Middeldorp
Proceedings of the 17th International Workshop on Functional and (Constraint) Logic Programming (WFLP 2008), Electronic Notes in Theoretical Computer Science 246, pp. 199 – 214, 2009.

Beyond Dependency Graphs
Martin Korp and Aart Middeldorp
Proceedings of the 22nd International Conference on Automated Deduction (CADE 2009), Lecture Notes in Artificial Intelligence 5663, pp. 339 – 354, 2009.

KBO Orientability
Harald Zankl, Nao Hirokawa, and Aart Middeldorp
Journal of Automated Reasoning 43(2), pp. 173 – 201, 2009.

The Hydra Battle and Cichon’s Principle
Georg Moser
Applicable Algebra in Engineering, Communication and Computing 20(2), pp. 133 – 158, 2009.

Loops under Strategies
René Thiemann and Christian Sternagel
Proceedings of the 20th International Conference on Rewriting Techniques and Applications (RTA 2009), Lecture Notes in Computer Science 5595, pp. 17 – 31, 2009.

Dependency Pairs and Polynomial Path Orders
Martin Avanzini and Georg Moser
Proceedings of the 20th International Conference on Rewriting Techniques and Applications (RTA 2009), Lecture Notes in Computer Science 5595, pp. 48 – 62, 2009.

The Derivational Complexity Induced by the Dependency Pair Method
Georg Moser and Andreas Schnabl
Proceedings of the 20th International Conference on Rewriting Techniques and Applications (RTA 2009), Lecture Notes in Computer Science 5595, pp. 255 – 269, 2009.

Tyrolean Termination Tool 2
Martin Korp, Christian Sternagel, Harald Zankl, and Aart Middeldorp
Proceedings of the 20th International Conference on Rewriting Techniques and Applications (RTA 2009), Lecture Notes in Computer Science 5595, pp. 295 – 304, 2009.

8th International Workshop on Reduction Strategies in Rewriting and Programming (WRS 2008)
Aart Middeldorp (ed.)
special issue, Electronic Notes in Theoretical Computer Science 237, pp. 1 – 126, 2009.

Constraint-Based Multi-Completion Procedures for Term Rewriting Systems
Haruhiko Sato, Masahito Kurihara, Sarah Winkler, and Aart Middeldorp
IEICI Transactions on Information and Systems E92-D(2), pp. 220 – 234, 2009.

From Outermost Termination to Innermost Termination
René Thiemann
Proceedings of the 35th International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM 2009), Lecture Notes in Computer Science 5404, pp. 533 – 545, 2009.

Complexity Analysis of Term Rewriting Based on Matrix and Context Dependent Interpretations
Georg Moser, Andreas Schnabl, and Johannes Waldmann
Proceedings of the 28th International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2008),   pp. 304 – 315, 2008.

Uncurrying for Termination
Nao Hirokawa, Aart Middeldorp, and Harald Zankl
Proceedings of the 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2008), Lecture Notes in Artificial Intelligence 5330, pp. 667 – 681, 2008.

Complexity, Graphs, and the Dependency Pair Method
Nao Hirokawa and Georg Moser
Proceedings of the 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2008), Lecture Notes in Artificial Intelligence 5330, pp. 652 – 666, 2008.

Improving Context-Sensitive Dependency Pairs
Beatriz Alarcón, Fabian Emmes, Carsten Fuhs, Jürgen Giesl, Raúl Gutiérrez, Salvador Lucas, Peter Schneider-Kamp, and René Thiemann
Proceedings of the 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2008), Lecture Notes in Artificial Intelligence 5330, pp. 636 – 651, 2008.

Match-Bounds with Dependency Pairs for Proving Termination of Rewrite Systems
Martin Korp and Aart Middeldorp
Proceedings of the 2nd International Conference on Language and Automata Theory and Application (LATA 2008), Lecture Notes in Computer Science 5196, pp. 321 – 332, 2008.

Multi-Completion with Termination Tools (System Description)
Haruhiko Sato, Sarah Winkler, Masahito Kurihara, and Aart Middeldorp
Proceedings of the 4th International Joint Conference on Automated Reasoning (IJCAR 2008), Lecture Notes in Artificial Intelligence 5195, pp. 306 – 312, 2008.

Automated Implicit Computational Complexity Analysis (System Description)
Martin Avanzini, Georg Moser, and Andreas Schnabl
Proceedings of the 4th International Joint Conference on Automated Reasoning (IJCAR 2008), Lecture Notes in Artificial Intelligence 5195, pp. 132 – 139, 2008.

Automated Complexity Analysis Based on the Dependency Pair Method
Nao Hirokawa and Georg Moser
Proceedings of the 4th International Joint Conference on Automated Reasoning (IJCAR 2008), Lecture Notes in Artificial Intelligence 5195, pp. 364 – 380, 2008.

Increasing Interpretations
Harald Zankl and Aart Middeldorp
Proceedings of the 9th International Conference on Artificial Intelligence and Symbolic Computation (AISC 2008), Lecture Notes in Artificial Intelligence 5144, pp. 191 – 205, 2008.

Proving Quadratic Derivational Complexities using Context Dependent Interpretations
Georg Moser and Andreas Schnabl
Proceedings of the 19th International Conference on Rewriting Techniques and Applications (RTA 2008), Lecture Notes in Computer Science 5117, pp. 276 – 290, 2008.

Deciding Innermost Loops
René Thiemann, Jürgen Giesl, and Peter Schneider-Kamp
Proceedings of the 19th International Conference on Rewriting Techniques and Applications (RTA 2008), Lecture Notes in Computer Science 5117, pp. 366 – 380, 2008.

Root-Labeling
Christian Sternagel and Aart Middeldorp
Proceedings of the 19th International Conference on Rewriting Techniques and Applications (RTA 2008), Lecture Notes in Computer Science 5117, pp. 336 – 350, 2008.

Maximal Termination
Carsten Fuhs, Jürgen Giesl, Aart Middeldorp, Peter Schneider-Kamp, René Thiemann, and Harald Zankl
Proceedings of the 19th International Conference on Rewriting Techniques and Applications (RTA 2008), Lecture Notes in Computer Science 5117, pp. 110 – 125, 2008.

Complexity Analysis by Rewriting
Martin Avanzini and Georg Moser
Proceedings of the 9th International Symposium on Functional and Logic Programming (FLOPS 2008), Lecture Notes in Computer Science 4989, pp. 130 – 146, 2008.

Innermost Termination of Rewrite Systems by Labeling
René Thiemann and Aart Middeldorp
Proceedings of the 7th International Workshop on Reduction Strategies in Rewriting and Programming (WRS 2007), Electronic Notes in Theoretical Computer Science 204, pp. 3 – 19, 2008.

A Database Approach to Distributed State Space Generation
Stefan Blom, Bert Lisser, Jaco van de Pol, and Michael Weber
Proceedings of the 6th International Workshop on Parallel and Distributed Methods in Verification (PDMC 2007), Electronic Notes in Theoretical Computer Science 198(1), pp. 17 – 32, 2008.

Adding Constants to String Rewriting
René Thiemann, Hans Zantema, Jürgen Giesl, and Peter Schneider-Kamp
Applicable Algebra in Engineering, Communication and Computing 19(1), pp. 27 – 38, 2008.

A Mechanized Proof of the Basic Perturbation Lemma
Jesús Aransay, Clemens Ballarin, and Julio Rubio
Journal of Automated Reasoning 40(4), pp. 271 – 292, 2008.

Simulated Time for Host-Based Testing with TTCN-3
Stefan Blom, Thomas Deiß, Natalia Ioustinova, Ari Kontio, Jaco van de Pol, Axel Rennoch, and Natalia Sidorova
Software Testing, Verification and Reliability 18(1), pp. 29 – 49, 2007.

TTCN-3 for Distributed Testing Embedded Software
Stefan Blom, Thomas Deiß, Natalia Ioustinova, Ari Kontio, Jaco van de Pol, Axel Rennoch, and Natalia Sidorova
Proceedings of the 6th International Andrei Ershov Memorial Conference: Perspectives of System Informatics (PSI 2006), Lecture Notes in Computer Science 4378, pp. 98 – 111, 2007.

Predictive Labeling with Dependency Pairs using SAT
Adam Koprowski and Aart Middeldorp
Proceedings of the 21st International Conference on Automated Deduction (CADE 2007), Lecture Notes in Artificial Intelligence 4603, pp. 410 – 425, 2007.

Satisfying KBO Constraints
Harald Zankl and Aart Middeldorp
Proceedings of the 18th International Conference on Rewriting Techniques and Applications (RTA 2007), Lecture Notes in Computer Science 4533, pp. 389 – 403, 2007.

Proving Termination of Rewrite Systems using Bounds
Martin Korp and Aart Middeldorp
Proceedings of the 18th International Conference on Rewriting Techniques and Applications (RTA 2007), Lecture Notes in Computer Science 4533, pp. 273 – 287, 2007.

The Hydra Battle Revisited
Nachum Dershowitz and Georg Moser
Rewriting, Computation and Proof; Essays Dedicated to Jean-Pierre Jouannaud on the Occasion of his 60th Birthday, Lecture Notes in Computer Science 4600, pp. 1 – 27, 2007.

SAT Solving for Termination Analysis with Polynomial Interpretations
Carsten Fuhs, Jürgen Giesl, Aart Middeldorp, Peter Schneider-Kamp, René Thiemann, and Harald Zankl
Proceedings of the 10th International Conference on Theory and Applications of Satisfiability Testing (SAT 2007), Lecture Notes in Computer Science 4501, pp. 340 – 254, 2007.

Tyrolean Termination Tool: Techniques and Features
Nao Hirokawa and Aart Middeldorp
Information and Computation 205(4), pp. 474 – 511, 2007.

Distributed Analysis with µCRL: A Compendium of Case Studies
Stefan Blom, Jens R. Calamé, Bert Lisser, Simona Orzan, Jun Pang, Jaco van de Pol, Mohammad Torabi Dashti, and Anton J. Wijs
Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2007), Lecture Notes in Computer Science 4424, pp. 683 – 689, 2007.

Constraints for Argument Filterings
Harald Zankl, Nao Hirokawa, and Aart Middeldorp
Proceedings of the 33rd International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM 2007), Lecture Notes in Computer Science 4362, pp. 579 – 590, 2007.

Derivational Complexity of Knuth-Bendix Orders Revisited
Georg Moser
Proceedings of the 13th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2006), Lecture Notes in Computer Science 4246, pp. 75 – 89, 2006.

Ackermann’s Substitution Method (remixed)
Georg Moser
Annals of Pure and Applied Logic 142(1-3), pp. 1 – 18, 2006.

Uncurrying for Termination
Nao Hirokawa and Aart Middeldorp
Proceedings of the 3rd International Workshop on Higher-Order Rewriting (HOR 2006),   pp. 19 – 24, 2006.

Predictive Labeling
Nao Hirokawa and Aart Middeldorp
Proceedings of the 17th International Conference on Rewriting Techniques and Applications (RTA 2006), Lecture Notes in Computer Science 4098, pp. 313 – 327, 2006.

Simulated Time for Testing Railway Interlockings with TTCN-3
Stefan Blom, Natalia Ioustinova, Jaco van de Pol, Axel Rennoch, and Natalia Sidorova
Proceedings of the 5th International Workshop on Formal Approaches to Software Testing (FATES 2005), Lecture Notes in Computer Science 3997, pp. 1 – 15, 2006.

Automated Termination Analysis for Term Rewriting
Nao Hirokawa
PhD thesis, University of Innsbruck, 2006.

Herbrand’s Theorem and Term Induction
Matthias Baaz and Georg Moser
Archive for Mathematical Logic 45(4), pp. 447 – 503, 2006.

The Epsilon Calculus and Herbrand Complexity
Georg Moser and Richard Zach
Studia Logica 82(1), pp. 133 – 155, 2006.

Skew and ω-Skew Confluence and Abstract Böhm Semantics
Zena M. Ariola and Stefan Blom
Processes, Terms and Cycles: Steps on the Road to Infinity; Essays Dedicated to Jan Willem Klop on the Occasion of his 60th Birthday, Lecture Notes in Computer Science 3838, pp. 368 – 403, 2005.

Processes, Terms and Cycles: Steps on the Road to Infinity
Aart Middeldorp, Vincent van Oostrom, Femke van Raamsdonk, and Roel de Vrijer (eds.)
Essays Dedicated to Jan Willem Klop on the Occasion of his 60th Birthday, Lecture Notes in Computer Science 3838, 2005.

Proofs of Termination of Rewrite Systems for Polytime Functions
Toshiyasu Arai and Georg Moser
Proceedings of the 25th International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2005), Lecture Notes in Computer Science 3821, pp. 529 – 540, 2005.

Automating the Dependency Pair Method
Nao Hirokawa and Aart Middeldorp
Information and Computation 199(1,2), pp. 172 – 199, 2005.

Tyrolean Termination Tool
Nao Hirokawa and Aart Middeldorp
Proceedings of the 16th International Conference on Rewriting Techniques and Applications (RTA 2005), Lecture Notes in Computer Science 3467, pp. 175 – 184, 2005.

Decidable Call-by-Need Computations in Term Rewriting
Irène Durand and Aart Middeldorp
Information and Computation 196(2), pp. 95 – 126, 2005.

Polynomial Interpretations with Negative Coefficients
Nao Hirokawa and Aart Middeldorp
Proceedings of the 7th International Conference on Artificial Intelligence and Symbolic Mathematical Computation (AISC 2004), Lecture Notes in Artificial Intelligence 3249, pp. 185 – 198, 2004.

New Completeness Results for Lazy Conditional Narrowing
Mircea Marin and Aart Middeldorp
Proceedings of the 6th ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP 2004),   pp. 120 – 131, 2004.

Transformation Techniques for Context-Sensitive Rewrite Systems
Jürgen Giesl and Aart Middeldorp
Journal of Functional Programming 14(4), pp. 379 – 427, 2004.

Dependency Pairs Revisited
Nao Hirokawa and Aart Middeldorp
Proceedings of the 15th International Conference on Rewriting Techniques and Applications (RTA 2004), Lecture Notes in Computer Science 3091, pp. 249 – 268, 2004.