| Publication | Date of Publication | Type |
|---|
| Certifying the weighted path order (invited talk) | 2026-02-24 | Paper |
Reachability Analysis for Termination and Confluence of Rewriting
Tools and Algorithms for the Construction and Analysis of Systems | 2023-11-24 | Paper |
A Mechanized Proof of Higman’s Lemma by Open Induction
Trends in Logic | 2020-07-08 | Paper |
| scientific article; zbMATH DE number 7204438 (Why is no real title available?) | 2020-05-26 | Paper |
| Certified equational reasoning via ordered completion | 2020-03-10 | Paper |
| Certified Kruskal's tree theorem | 2019-09-18 | Paper |
Abstract completion, formalized
(available as arXiv preprint) | 2019-09-13 | Paper |
| A formally verified solver for homogeneous linear Diophantine equations | 2018-10-04 | Paper |
| Foundational (co)datatypes and (co)recursion for higher-order logic | 2018-01-04 | Paper |
| Certifying confluence of almost orthogonal CTRSs via exact tree automata completion | 2017-10-17 | Paper |
| Certifying confluence of quasi-decreasing strongly deterministic conditional term rewrite systems | 2017-09-22 | Paper |
| AC dependency pairs revisited | 2017-07-19 | Paper |
| Certification of complexity proofs using CeTA | 2017-07-12 | Paper |
| Formalizing Knuth-Bendix orders and Knuth-Bendix completion | 2017-02-01 | Paper |
| A framework for developing stand-alone certifiers | 2016-08-01 | Paper |
Deriving comparators and show functions in Isabelle/HOL
Interactive Theorem Proving | 2015-09-14 | Paper |
Proof pearl: A mechanized proof of GHC's mergesort
Journal of Automated Reasoning | 2015-06-23 | Paper |
Transforming SAT into termination of rewriting
Electronic Notes in Theoretical Computer Science | 2015-04-09 | Paper |
Certified Kruskal's tree theorem
Certified Programs and Proofs | 2015-01-13 | Paper |
A New and Formalized Proof of Abstract Completion
Interactive Theorem Proving | 2014-09-08 | Paper |
Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs
Lecture Notes in Computer Science | 2014-07-24 | Paper |
Certification of nontermination proofs
Interactive Theorem Proving | 2012-09-20 | Paper |
| Certified subterm criterion and certified usable rules | 2012-04-25 | Paper |
| Modular and certified semantic labeling and unlabeling | 2012-04-24 | Paper |
Generalized and formalized uncurrying
Frontiers of Combining Systems | 2011-10-07 | Paper |
Termination of Isabelle functions via termination of rewriting
Interactive Theorem Proving | 2011-08-17 | Paper |
Signature extensions preserve termination. An alternative proof via dependency pairs
Computer Science Logic | 2010-09-03 | Paper |
Finding and certifying loops
SOFSEM 2010: Theory and Practice of Computer Science | 2010-01-28 | Paper |
Certification of Termination Proofs Using CeTA
Lecture Notes in Computer Science | 2009-10-20 | Paper |
Loops under Strategies
Rewriting Techniques and Applications | 2009-06-30 | Paper |
Root-Labeling
Rewriting Techniques and Applications | 2008-08-28 | Paper |
