Alphabetical List of Titles

1. A Relative Dependency Pair Framework
2. Abstract Rewriting
3. Automatic Certification of Termination Proofs
4. CeTA - A Tool for Certified Termination Analysis
5. Certification extends Termination Techniques
6. Certification of Nontermination Proofs
7. Certification of Termination Proofs using CeTA
8. Certified Subterm Criterion and Certified Usable Rules
9. Efficient Mergesort
10. Executable Matrix Operations on Matrices of Arbitrary Dimensions
11. Executable Multivariate Polynomials
12. Executable Transitive Closures of Finite Relations
13. Finding and Certifying Loops
14. Generalized and Formalized Uncurrying
15. Loops under Strategies
16. Loops under Strategies ... Continued
17. Loops under Strategies ... Continued
18. Modular and Certified Semantic Labeling and Unlabeling
19. Recording Completion for Finding and Certifying Proofs in Equational Logic
20. Root-Labeling
21. Signature Extensions Preserve Termination - An Alternative Proof via Dependency Pairs
22. Termination of Isabelle Functions via Termination of Rewriting
23. Transforming SAT into Termination of Rewriting
24. Tyrolean Termination Tool 2
25. Well-Quasi-Orders

Papers in Proceedings

• Christian Sternagel and René Thiemann
  Certification of Nontermination Proofs
  In Proceedings of the 3rd International Conference on Interactive Theorem Proving (ITP '12),
  Lecture Notes in Computer Science, to appear.
• Christian Sternagel and René Thiemann
  Generalized and Formalized Uncurrying
  In Proceedings of the 8th International Symposium on Frontiers of Combining Systems (FroCoS '11),
  Lecture Notes in Artificial Intelligence 6989, pp. 243–258, 2011.© Springer-Verlag
• Alexander Krauss, Christian Sternagel, René Thiemann, Carsten Fuhs, and Jürgen Giesl
  Termination of Isabelle Functions via Termination of Rewriting
  In Proceedings of the 2nd International Conference on Interactive Theorem Proving (ITP '11),
  Lecture Notes in Computer Science 6898, pp. 152–167, 2011.© Springer-Verlag
• Christian Sternagel and René Thiemann
  Modular and Certified Semantic Labeling and Unlabeling
  In Proceedings of the 22nd International Conference on Rewriting Techniques and Applications (RTA '11),
  Leibniz International Proceedings in Informatics 10, pp. 329–344, 2011. Schloss Dagstuhl
• René Thiemann, Christian Sternagel, Jürgen Giesl, and Peter Schneider-Kamp
  Loops under Strategies ... Continued
  In Proceedings of the 1st International Workshop on Strategies in Rewriting, Poving, and Programming (IWS '10),
  Electronic Proceedings in Theoretical Computer Science 44, pp. 51–65, 2010. 10.4204/EPTCS.44
• Christian Sternagel and René Thiemann
  Signature Extensions Preserve Termination - An Alternative Proof via Dependency Pairs
  In Proceedings of the 19th EACSL Annual Conference on Computer Science Logic (CSL '10),
  Lecture Notes in Computer Science 6247, pp. 514–528, 2010.© Springer-Verlag
• Christian Sternagel and René Thiemann
  Certified Subterm Criterion and Certified Usable Rules
  In Proceedings of the 21st International Conference on Rewriting Techniques and Applications (RTA '10),
  Leibniz International Proceedings in Informatics 6, pp. 325–340, 2010. Schloss Dagstuhl
• Harald Zankl, Christian Sternagel, Dieter Hofbauer, and Aart Middeldorp
  Finding and Certifying Loops
  In Proceedings of the 36th International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM '10),
  Lecture Notes in Computer Science 5901, pp. 755–766, 2010.© Springer-Verlag
• René Thiemann and Christian Sternagel
  Certification of Termination Proofs using CeTA
  In Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs '09),
  Lecture Notes in Computer Science 5674, pp. 452–468, 2009.© Springer-Verlag
• Harald Zankl, Christian Sternagel, and Aart Middeldorp
  Transforming SAT into Termination of Rewriting
  In Proceedings of the 17th International Workshop on Functional and (Constraint) Logic Programming (WFLP '08),
  Electronic Notes in Theoretical Computer Science 246, pp. 199–214, 2009.© Elsevier B.V.
• Martin Korp, Christian Sternagel, Harald Zankl, and Aart Middeldorp
  Tyrolean Termination Tool 2
  In Proceedings of the 20th International Conference on Rewriting Techniques and Applications (RTA '09),
  Lecture Notes in Computer Science 5595, pp. 295–304, 2009.© Springer-Verlag
• René Thiemann and Christian Sternagel
  Loops under Strategies
  In Proceedings of the 20th International Conference on Rewriting Techniques and Applications (RTA '09),
  Lecture Notes in Computer Science 5595, pp. 17–31, 2009.© Springer-Verlag
• Christian Sternagel and Aart Middeldorp
  Root-Labeling
  In Proceedings of the 19th International Conference on Rewriting Techniques and Applications (RTA '08),
  Lecture Notes in Computer Science 5117, pp. 336–350, 2008.© Springer-Verlag
  erratum

Thesis

• Christian Sternagel
  Automatic Certification of Termination Proofs
  PhD Thesis, 2010.

Others

• Christian Sternagel
  Well-Quasi-Orders
  In Gerwin Klein, Tobias Nipkow, and Lawrence Paulson, editors, The Archive of Formal Proofs.
  April 2012. Formal proof development.
• Thomas Sternagel, René Thiemann, Harald Zankl, and Christian Sternagel
  Recording Completion for Finding and Certifying Proofs in Equational Logic
  In Proceedings of the 1st International Workshop on Confluence (IWC '12),
  to appear.
• Christian Sternagel and René Thiemann
  A Relative Dependency Pair Framework
  In Proceedings of the 13rd International Workshop on Termination (WST '12),
  pp. 79–83, 2012.
• Christian Sternagel
  Efficient Mergesort
  In Gerwin Klein, Tobias Nipkow, and Lawrence Paulson, editors, The Archive of Formal Proofs.
  November 2011. Formal proof development.
• Christian Sternagel and René Thiemann
  Executable Transitive Closures of Finite Relations
  In Gerwin Klein, Tobias Nipkow, and Lawrence Paulson, editors, The Archive of Formal Proofs.
  March 2011. Formal proof development.
• Christian Sternagel and René Thiemann
  Executable Multivariate Polynomials
  In Gerwin Klein, Tobias Nipkow, and Lawrence Paulson, editors, The Archive of Formal Proofs.
  August 2010. Formal proof development.
• Christian Sternagel and René Thiemann
  Certification extends Termination Techniques
  In Proceedings of the 11st International Workshop on Termination (WST '10),
  2010.
• René Thiemann, Jürgen Giesl, Peter Schneider-Kamp, and Christian Sternagel
  Loops under Strategies ... Continued
  In Proceedings of the 1st International Workshop on Strategies in Rewriting, Poving, and Programming (IWS '10),
  2010.
• Christian Sternagel and René Thiemann
  Executable Matrix Operations on Matrices of Arbitrary Dimensions
  In Gerwin Klein, Tobias Nipkow, and Lawrence Paulson, editors, The Archive of Formal Proofs.
  June 2010. Formal proof development.
• Christian Sternagel and René Thiemann
  Abstract Rewriting
  In Gerwin Klein, Tobias Nipkow, and Lawrence Paulson, editors, The Archive of Formal Proofs.
  June 2010. Formal proof development.
• Christian Sternagel, René Thiemann, Sarah Winkler, and Harald Zankl
  CeTA - A Tool for Certified Termination Analysis
  In Proceedings of the 10th International Workshop on Termination (WST '09),
  2009.