Christian Sternagel

General Information

visiting researcher

address:	School of Information Science Japan Advanced Institute of Science and Technology 1-1 Asahidai, Nomi, Ishikawa, 923-1292, Japan
email:	c-sterna@jaist.ac.jp
research group:	Ogawa-Hirokawa Laboratory (room I-51)
research interests:	interactive theorem proving verification of (functional) programs term rewriting (termination and certification of termination proofs) ttt2   IsaFoR/CeTA

Publications

Journal Articles

• Christian Sternagel
  Proof Pearl - A Mechanized Proof of GHC's Mergesort
  Journal of Automated Reasoning, 2012. Springer-Verlag
  doi:10.1007/s10817-012-9260-7

Papers in Proceedings

• Christian Sternagel and René Thiemann
  Formalizing Knuth-Bendix Orders and Knuth-Bendix Completion
  In Proceedings of the 24th International Conference on Rewriting Techniques and Applications (RTA '13),
  Leibniz International Proceedings in Informatics, 2013. Schloss Dagstuhl
• 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 7406, pp. 266–282, 2012. © Springer-Verlag
  doi:10.1007/978-3-642-32347-8_18
• 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
  doi:10.1007/978-3-642-24364-6_17
• 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
  doi:10.1007/978-3-642-22863-6_13
• 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
  doi:10.4230/LIPIcs.RTA.2011.329
• 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.
  doi: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
  doi:10.1007/978-3-642-15205-4_39
• 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
  doi:10.4230/LIPIcs.RTA.2010.325
• 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
  doi:10.1007/978-3-642-11266-9_63
• 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
  doi:10.1007/978-3-642-03359-9_31
• 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.
  doi:10.1016/j.entcs.2009.07.023
• 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
  doi:10.1007/978-3-642-02348-4_21
• 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
  doi:10.1007/978-3-642-02348-4_2
• 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
  doi:10.1007/978-3-540-70590-1_23
  erratum

Thesis

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

Others

• Mizuhito Ogawa and Christian Sternagel
  Open Induction
  In Gerwin Klein, Tobias Nipkow, and Lawrence Paulson, editors, The Archive of Formal Proofs
  November 2012. Formal proof development.
  afp-devel: Open_Induction
• Christian Sternagel
  Getting Started with Isabelle/jEdit
  In Isabelle Users Workshop 2012 (IUW '12),
  2012.
  arXiv: 1208.1368
• Christian Sternagel
  A Locale for Minimal Bad Sequences
  In Isabelle Users Workshop 2012 (IUW '12),
  2012.
  arXiv: 1208.1366
• Christian Sternagel
  Well-Quasi-Orders
  In Gerwin Klein, Tobias Nipkow, and Lawrence Paulson, editors, The Archive of Formal Proofs
  April 2012. Formal proof development.
  afp-devel: Well_Quasi_Orders
• 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),
  pp. 31–36, 2012.
  arXiv: 1208.1597
• Christian Sternagel and René Thiemann
  A Relative Dependency Pair Framework
  In Proceedings of the 13th International Workshop on Termination (WST '12),
  pp. 79–83, 2012.
  arXiv: 1208.1595
• Christian Sternagel
  Efficient Mergesort
  In Gerwin Klein, Tobias Nipkow, and Lawrence Paulson, editors, The Archive of Formal Proofs
  November 2011. Formal proof development.
  afp: Efficient-Mergesort
• 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.
  afp: Transitive-Closure
• 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.
  afp: Polynomials
• Christian Sternagel and René Thiemann
  Certification extends Termination Techniques
  In Proceedings of the 11th International Workshop on Termination (WST '10),
  2010.
  arXiv: 1208.1594
• 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.
  arXiv: 1012.5563
• 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.
  afp: Matrix
• 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.
  afp: Abstract-Rewriting
• 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.
  arXiv: 1208.1591

Drafts

• Christian Sternagel
  A Formal Proof of Kruskal's Tree Theorem in Isabelle/HOL
  Draft, 2013.

Software