Books

• Tobias Nipkow, Jasmin Blanchette, Manuel Eberl, Alejandro Gómez-Londoño, Peter Lammich, Christian Sternagel, Simon Wimmer, and Bohua Zhan
  Functional Algorithms, Verified!
  2021.
  http://functional-algorithms-verified.org/

Journal Articles

• Nao Hirokawa, Aart Middeldorp, Christian Sternagel, and Sarah Winkler
  Abstract Completion, Formalized
  Logical Methods in Computer Science 15(3), pp. 19:1–19:42, 2019.
  doi:10.23638/LMCS-15(3:19)2019
• Christian Sternagel and René Thiemann
  A Framework for Developing Stand-Alone Certifiers
  Electronic Notes in Theoretical Computer Science 312, pp. 51–67, 2015. © Elsevier B.V.
  doi:10.1016/j.entcs.2015.04.004
• Christian Sternagel
  Certified Kruskal's Tree Theorem
  Journal of Formalized Reasoning 7(1), pp. 45–62, 2014.
  doi:10.6092/issn.1972-5787/4213
• Christian Sternagel
  Proof Pearl - A Mechanized Proof of GHC's Mergesort
  Journal of Automated Reasoning 51(4), pp. 357–370, 2013. Springer-Verlag (Open Access)
  doi:10.1007/s10817-012-9260-7
• Harald Zankl, Christian Sternagel, and Aart Middeldorp
  Transforming SAT into Termination of Rewriting
  Electronic Notes in Theoretical Computer Science 246, pp. 199–214, 2009. © Elsevier B.V.
  doi:10.1016/j.entcs.2009.07.023

Book Chapters

• Christian Sternagel
  A Mechanized Proof of Higman's Lemma by Open Induction
  In Well-Quasi Orders in Computation, Logic, Language and Reasoning,
  2019. © Springer-Verlag
  doi:10.1007/978-3-030-30229-0_12

Papers in Proceedings

• Christian Sternagel and Sarah Winkler
  Certified Equational Reasoning via Ordered Completion
  In Proceedings of the 27th International Confluence on Automated Deduction (CADE-27),
  Lecture Notes in Computer Science 11716, pp. 508–525, 2019. Springer-Verlag (Open Access)
  doi:10.1007/978-3-030-29436-6_30
• Jürgen Giesl, Albert Rubio, Christian Sternagel, Johannes Waldmann, and Akihisa Yamada
  The Termination and Complexity Competition
  In Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '19),
  Lecture Notes in Computer Science 11429, pp. 156–166, 2019. Springer-Verlag (Open Access)
  doi:10.1007/978-3-030-17502-3_10
• Christian Sternagel and Akihisa Yamada
  Reachability Analysis for Termination and Confluence of Rewriting
  In Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '19),
  Lecture Notes in Computer Science 11427, pp. 262–278, 2019. Springer-Verlag (Open Access)
  doi:10.1007/978-3-030-17462-0_15
• Florian Meßner and Christian Sternagel
  nonreach - A Tool for Nonreachability Analysis
  In Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '19),
  Lecture Notes in Computer Science 11427, pp. 337–343, 2019. Springer-Verlag (Open Access)
  doi:10.1007/978-3-030-17462-0_19
• Alexander Lochmann and Christian Sternagel
  Certified ACKBO
  In Proceedings of the 8th International Conference on Certified Programs and Proofs (CPP '19),
  pp. 144–151, 2019. ACM (Open Access)
  doi:10.1145/3293880.3294099
• Florian Meßner, Julian Parsert, Jonas Schöpf, and Christian Sternagel
  A Formally Verified Solver for Homogeneous Linear Diophantine Equations
  In Proceedings of the 9th International Conference on Interactive Theorem Proving (ITP '18),
  Lecture Notes in Computer Science 10895, pp. 441–458, 2018. Springer-Verlag (Open Access)
  doi:10.1007/978-3-319-94821-8_26
• Julian Biendarra, Jasmin Blanchette, Aymeric Bouzy, Martin Desharnais, Mathias Fleury, Johannes Hölzl, Ondřej Kunčar, Andreas Lochbihler, Fabian Meier, Lorenz Panny, Andrei Popescu, Christian Sternagel, René Thiemann, and Dmitriy Traytel
  Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic
  In Proceedings of the 14th International Symposium on Frontiers of Combining Systems (FroCoS '17),
  Lecture Notes in Computer Science 10483, pp. 3–21, 2017. © Springer-Verlag
  doi:10.1007/978-3-319-66167-4_1
• Nao Hirokawa, Aart Middeldorp, Christian Sternagel, and Sarah Winkler
  Infinite Runs in Abstract Completion
  In Proceedings of the 2nd International Conference on Formal Structures for Computation and Deduction (FSCD '17),
  Leibniz International Proceedings in Informatics 84, pp. 19:1–19:16, 2017. Schloss Dagstuhl
  doi:10.4230/LIPIcs.FSCD.2017.19
• Christian Sternagel and Thomas Sternagel
  Certifying Confluence of Quasi-Decreasing Strongly Deterministic Conditional Term Rewrite Systems
  In Proceedings of the 26th International Confluence on Automated Deduction (CADE-26),
  Lecture Notes in Computer Science 10395, pp. 413–431, 2017. Springer-Verlag (Open Access)
  doi:10.1007/978-3-319-63046-5_26
• Akihisa Yamada, Christian Sternagel, René Thiemann, and Keiichirou Kusakari
  AC Dependency Pairs Revisited
  In Proceedings of the 25th EACSL Annual Conference on Computer Science Logic (CSL '16),
  Leibniz International Proceedings in Informatics 62, pp. 8:1–8:16, 2016. Schloss Dagstuhl
  doi:10.4230/LIPIcs.CSL.2016.8
• Christian Sternagel and Thomas Sternagel
  Certifying Confluence of Almost Orthogonal CTRSs via Exact Tree Automata Completion
  In Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD '16),
  Leibniz International Proceedings in Informatics 52, pp. 29:1–29:16, 2016. Schloss Dagstuhl
  doi:10.4230/LIPIcs.FSCD.2016.29
• Christian Sternagel and René Thiemann
  Deriving Comparators and Show Functions in Isabelle/HOL
  In Proceedings of the 6th International Conference on Interactive Theorem Proving (ITP '15),
  Lecture Notes in Computer Science 9236, pp. 421–437, 2015. © Springer-Verlag
  doi:10.1007/978-3-319-22102-1_28
• Martin Avanzini, Christian Sternagel, and René Thiemann
  Certification of Complexity Proofs using CeTA
  In Proceedings of the 26th International Conference on Rewriting Techniques and Applications (RTA '15),
  Leibniz International Proceedings in Informatics 36, pp. 23–39, 2015. Schloss Dagstuhl
  doi:10.4230/LIPIcs.RTA.2015.23
• Christian Sternagel and René Thiemann
  The Certification Problem Format
  In Proceedings of the 11th Workshop on User Interfaces for Theorem Provers (UITP '14),
  Electronic Proceedings in Theoretical Computer Science 167, pp. 61–72, 2014.
  doi:10.4204/EPTCS.167.8
• Christian Sternagel and René Thiemann
  Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs
  In Proceedings of the Joint 25th International Conference on Rewriting Techniques and Applications (RTA '14) and 12th International Conference on Typed Lambda Calculi and Applications (TLCA '14),
  Lecture Notes in Computer Science 8560, pp. 441–455, 2014. © Springer-Verlag
  doi:10.1007/978-3-319-08918-8_30
• Nao Hirokawa, Aart Middeldorp, and Christian Sternagel
  A New and Formalized Proof of Abstract Completion
  In Proceedings of the 5th International Conference on Interactive Theorem Proving (ITP '14),
  Lecture Notes in Computer Science 8558, pp. 292–307, 2014. © Springer-Verlag
  doi:10.1007/978-3-319-08970-6_19
• Christian Sternagel
  Certified Kruskal's Tree Theorem
  In Proceedings of the 3rd International Conference on Certified Programs and Proofs (CPP '13),
  Lecture Notes in Computer Science 8307, pp. 178–193, 2013. © Springer-Verlag
  doi:10.1007/978-3-319-03545-1_12
• 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 21, pp. 287–302, 2013. Schloss Dagstuhl
  doi:10.4230/LIPIcs.RTA.2013287
• 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.4
• 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
• 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
  Certified Term Rewriting
  Habilitation Thesis, 2020.
• Christian Sternagel
  Automatic Certification of Termination Proofs
  PhD Thesis, 2010.

Others

• Bertram Felgenhauer, Franziska Rapp, Christian Sternagel, and Sarah Winkler
  CoCo 2018 Participant: CeTA 2.33
  In Proceedings of the 7th International Workshop on Confluence (IWC '18),
  2018.
• Florian Meßner and Christian Sternagel
  TermComp 2018 Participant: TTT2
  In Proceedings of the 16th International Workshop on Termination (WST '18),
  2018.
• Thomas Sternagel, Christian Sternagel, and Aart Middeldorp
  CoCo 2018 Participant: ConCon 1.5
  In Proceedings of the 7th International Workshop on Confluence (IWC '18),
  2018.
• Jonas Schöpf and Christian Sternagel
  TTT2 with Termination Templates for Teaching
  In Proceedings of the 16th International Workshop on Termination (WST '18),
  2018.
  arXiv: 1806.05040
• Christian Sternagel and Sarah Winkler
  Certified Ordered Completion
  In Proceedings of the 7th International Workshop on Confluence (IWC '18),
  2018.
  arXiv: 1805.10090
• Christian Sternagel
  The remote_build Tool
  In Isabelle Workshop 2018 (Isabelle '18),
  2018.
  arXiv: 1805.07195
• Christian Sternagel and René Thiemann
  First-Order Terms
  In Gerwin Klein, Tobias Nipkow, Lawrence Paulson, and René Thiemann, editors, The Archive of Formal Proofs
  February 2018. Formal proof development.
  afp: First_Order_Terms
• Florian Meßner, Julian Parsert, Jonas Schöpf, and Christian Sternagel
  Homogeneous Linear Diophantine Equations
  In Gerwin Klein, Tobias Nipkow, Lawrence Paulson, and René Thiemann, editors, The Archive of Formal Proofs
  October 2017. Formal proof development.
  afp: Diophantine_Eqns_Lin_Hom
• Julian Nagele, Christian Sternagel, and Thomas Sternagel
  CoCo 2017 Participant: CeTA 2.31
  In Proceedings of the 6th International Workshop on Confluence (IWC '17),
  2017.
• Thomas Sternagel, Christian Sternagel, and Aart Middeldorp
  CoCo 2017 Participant: ConCon 1.5
  In Proceedings of the 6th International Workshop on Confluence (IWC '17),
  2017.
• Aart Middeldorp and Christian Sternagel
  Formalized Ground Completion
  In Proceedings of the 6th International Workshop on Confluence (IWC '17),
  2017.
• Thomas Sternagel and Christian Sternagel
  Certified Non-Confluence with ConCon 1.5
  In Proceedings of the 6th International Workshop on Confluence (IWC '17),
  2017.
  arXiv: 1709.05162
• Joachim Breitner, Brian Huffman, Neil Mitchell, and Christian Sternagel
  HOLCF-Prelude
  In Gerwin Klein, Tobias Nipkow, Lawrence Paulson, and René Thiemann, editors, The Archive of Formal Proofs
  July 2017. Formal proof development.
  afp: HOLCF-Prelude
• Thomas Sternagel and Christian Sternagel
  Formalized Confluence of Quasi-Decreasing, Strongly Deterministic Conditional TRSs
  In Proceedings of the 5th International Workshop on Confluence (IWC '16),
  2016.
  arXiv: 1609.03341
• Julian Nagele, Vincent van Oostrom, and Christian Sternagel
  A Short Mechanized Proof of the Church-Rosser Theorem by the Z-property for the λβ-calculus in Nominal Isabelle
  In Proceedings of the 5th International Workshop on Confluence (IWC '16),
  2016.
  arXiv: 1609.03139
• Julian Nagele, Christian Sternagel, and Thomas Sternagel
  CoCo 2016 Participant: CeTA 2.28
  In Proceedings of the 5th International Workshop on Confluence (IWC '16),
  2016.
• Thomas Sternagel and Christian Sternagel
  A Characterization of Quasi-Decreasingness
  In Proceedings of the 15th International Workshop on Termination (WST '16),
  2016.
  arXiv: 1609.03345
• Christian Sternagel
  The Generalized Subterm Criterion in TTT2
  In Proceedings of the 15th International Workshop on Termination (WST '16),
  2016.
  arXiv: 1609.03432
• Christian Sternagel
  TTT2 @ TermComp'2016
  In Proceedings of the 15th International Workshop on Termination (WST '16),
  2016.
• Bertram Felgenhauer, Julian Nagele, Vincent van Oostrom, and Christian Sternagel
  The Z Property
  In Gerwin Klein, Tobias Nipkow, Lawrence Paulson, and René Thiemann, editors, The Archive of Formal Proofs
  June 2016. Formal proof development.
  afp: Rewriting_Z
• Julian Nagele, Christian Sternagel, Thomas Sternagel, René Thiemann, Sarah Winkler, and Harald Zankl
  CoCo 2015 Participant: CeTA 2.21
  In Proceedings of the 4th International Workshop on Confluence (IWC '15),
  2015.
• Christian Sternagel and Thomas Sternagel
  Level-Confluence of 3-CTRSs in Isabelle/HOL
  In Proceedings of the 4th International Workshop on Confluence (IWC '15),
  2015.
  arXiv: 1602.07115
• Christian Sternagel and René Thiemann
  Deriving class instances for datatypes
  In Gerwin Klein, Tobias Nipkow, Lawrence Paulson, and René Thiemann, editors, The Archive of Formal Proofs
  March 2015. Formal proof development.
  afp: Deriving
• Christian Sternagel and René Thiemann
  Xml
  In Gerwin Klein, Tobias Nipkow, Lawrence Paulson, and René Thiemann, editors, The Archive of Formal Proofs
  October 2014. Formal proof development.
  afp: XML
• Christian Sternagel and René Thiemann
  Certification Monads
  In Gerwin Klein, Tobias Nipkow, Lawrence Paulson, and René Thiemann, editors, The Archive of Formal Proofs
  October 2014. Formal proof development.
  afp: Certification_Monads
• Christian Sternagel
  Imperative Insertion Sort
  In Gerwin Klein, Tobias Nipkow, Lawrence Paulson, and René Thiemann, editors, The Archive of Formal Proofs
  September 2014. Formal proof development.
  afp: Imperative_Insertion_Sort
• Christian Sternagel and René Thiemann
  Haskell's Show Class in Isabelle/HOL
  In Gerwin Klein, Tobias Nipkow, Lawrence Paulson, and René Thiemann, editors, The Archive of Formal Proofs
  July 2014. Formal proof development.
  afp: Show
• Nao Hirokawa, Aart Middeldorp, and Christian Sternagel
  Normalization Equivalence of Rewrite Systems
  In Proceedings of the 3rd International Workshop on Confluence (IWC '14),
  2014.
• Bertram Felgenhauer, Martin Avanzini, and Christian Sternagel
  A Haskell Library for Term Rewriting
  In Proceedings of the 1st International Workshop on Haskell and Rewriting Techniques (HART '13),
  2013.
  arXiv: 1307.2328
• Joachim Breitner, Brian Huffman, Neil Mitchell, and Christian Sternagel
  Certified HLints with Isabelle/HOLCF-Prelude
  In Proceedings of the 1st International Workshop on Haskell and Rewriting Techniques (HART '13),
  2013.
  arXiv: 1306.1340
• Mizuhito Ogawa and Christian Sternagel
  Open Induction
  In Gerwin Klein, Tobias Nipkow, Lawrence Paulson, and René Thiemann, editors, The Archive of Formal Proofs
  November 2012. Formal proof development.
  afp: 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, Lawrence Paulson, and René Thiemann, editors, The Archive of Formal Proofs
  April 2012. Formal proof development.
  afp: 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 12th International Workshop on Termination (WST '12),
  pp. 79–83, 2012.
  arXiv: 1208.1595
• Christian Sternagel
  Efficient Mergesort
  In Gerwin Klein, Tobias Nipkow, Lawrence Paulson, and René Thiemann, 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, Lawrence Paulson, and René Thiemann, 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, Lawrence Paulson, and René Thiemann, 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, Lawrence Paulson, and René Thiemann, 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, Lawrence Paulson, and René Thiemann, 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 and Thomas Sternagel
  Certified Conditional Confluence
  Draft, 2019.

Alphabetical List of Titles

1. A Formally Verified Solver for Homogeneous Linear Diophantine Equations
2. A Haskell Library for Term Rewriting
3. A Framework for Developing Stand-Alone Certifiers
4. A New and Formalized Proof of Abstract Completion
5. A Locale for Minimal Bad Sequences
6. A Relative Dependency Pair Framework
7. A Short Mechanized Proof of the Church-Rosser Theorem by the Z-property for the λβ-calculus in Nominal Isabelle
8. A Mechanized Proof of Higman's Lemma by Open Induction
9. A Characterization of Quasi-Decreasingness
10. Abstract Completion, Formalized
11. Abstract Rewriting
12. AC Dependency Pairs Revisited
13. Automatic Certification of Termination Proofs
14. Certification extends Termination Techniques
15. Certification of Complexity Proofs using CeTA
16. Certification Monads
17. Certification of Termination Proofs using CeTA
18. Certification of Nontermination Proofs
19. Certified Subterm Criterion and Certified Usable Rules
20. Certified Non-Confluence with ConCon 1.5
21. Certified HLints with Isabelle/HOLCF-Prelude
22. Certified Kruskal's Tree Theorem
23. Certified Term Rewriting
24. Certified ACKBO
25. Certified Ordered Completion
26. Certified Kruskal's Tree Theorem
27. Certified Equational Reasoning via Ordered Completion
28. Certifying Confluence of Quasi-Decreasing Strongly Deterministic Conditional Term Rewrite Systems
29. Certifying Confluence of Almost Orthogonal CTRSs via Exact Tree Automata Completion
30. CeTA - A Tool for Certified Termination Analysis
31. CoCo 2015 Participant: CeTA 2.21
32. CoCo 2017 Participant: ConCon 1.5
33. CoCo 2018 Participant: CeTA 2.33
34. CoCo 2018 Participant: ConCon 1.5
35. CoCo 2016 Participant: CeTA 2.28
36. CoCo 2017 Participant: CeTA 2.31
37. Deriving class instances for datatypes
38. Deriving Comparators and Show Functions in Isabelle/HOL
39. Efficient Mergesort
40. Executable Transitive Closures of Finite Relations
41. Executable Multivariate Polynomials
42. Executable Matrix Operations on Matrices of Arbitrary Dimensions
43. Finding and Certifying Loops
44. First-Order Terms
45. Formalized Ground Completion
46. Formalized Confluence of Quasi-Decreasing, Strongly Deterministic Conditional TRSs
47. Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs
48. Formalizing Knuth-Bendix Orders and Knuth-Bendix Completion
49. Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic
50. Functional Algorithms, Verified!
51. Generalized and Formalized Uncurrying
52. Getting Started with Isabelle/jEdit
53. Haskell's Show Class in Isabelle/HOL
54. HOLCF-Prelude
55. Homogeneous Linear Diophantine Equations
56. Imperative Insertion Sort
57. Infinite Runs in Abstract Completion
58. Level-Confluence of 3-CTRSs in Isabelle/HOL
59. Loops under Strategies
60. Loops under Strategies ... Continued
61. Loops under Strategies ... Continued
62. Modular and Certified Semantic Labeling and Unlabeling
63. nonreach - A Tool for Nonreachability Analysis
64. Normalization Equivalence of Rewrite Systems
65. Open Induction
66. Proof Pearl - A Mechanized Proof of GHC's Mergesort
67. Reachability Analysis for Termination and Confluence of Rewriting
68. Recording Completion for Finding and Certifying Proofs in Equational Logic
69. Root-Labeling
70. Signature Extensions Preserve Termination - An Alternative Proof via Dependency Pairs
71. TermComp 2018 Participant: TTT2
72. Termination of Isabelle Functions via Termination of Rewriting
73. The Certification Problem Format
74. The remote_build Tool
75. The Z Property
76. The Termination and Complexity Competition
77. The Generalized Subterm Criterion in TTT2
78. Transforming SAT into Termination of Rewriting
79. TTT2 with Termination Templates for Teaching
80. TTT2 @ TermComp'2016
81. Tyrolean Termination Tool 2
82. Well-Quasi-Orders
83. Xml