Instantiation- and Learning-Based Methods in Equational Reasoning
Strong Modular Proof Assistance: Reasoning Across Theories
FORTissimo: Automating the First-Order Theory of Rewriting
The Fine Structure of Formal Proof Systems and their Computational Interpretations
Complexity Analysis-based Guaranteed Execution
From Confluence to Unique Normal Forms: Certification and Complexity
Certifying Termination and Complexity Proofs of Programs
Complexity Analysis of Higher-Order Rewrite Systems
Interactive Proof: Proof Translation, Premise Selection, Rewriting
Automated Complexity Analysis via Transformations
Constrained Rewriting and SMT: Emerging Trends in Rewriting
Formalizing Open Induction, The Tree Theorem, and Simple Termination
Structural and Computational Proof Theory
Improving Certifiers for Termination Proofs
Confluence: Automation, Certification, Extensions
Termination Tools in Automated Reasoning
Logic-Based Analysis of Computation