Logic/Rewriting

Reducing Rewrite Properties to Properties on Ground Terms
by Alexander Lochmann

The Generalized Multiset Ordering is NP-Complete
by René Thiemann and Lukas Schmidinger

First-Order Theory of Rewriting
by Alexander Lochmann and Bertram Felgenhauer

A Formalization of Weighted Path Orders and Recursive Path Orders
by Christian Sternagel, René Thiemann and Akihisa Yamada

A Formalization of Knuth–Bendix Orders
by Christian Sternagel and René Thiemann

Implementing the Goodstein Function in λ-Calculus
by Bertram Felgenhauer

A Verified Code Generator from Isabelle/HOL to CakeML
by Lars Hupel

Graph Saturation
by Sebastiaan J. C. Joosten

Formalization of the Embedding Path Order for Lambda-Free Higher-Order Terms
by Alexander Bentkamp

First-Order Terms
by Christian Sternagel and René Thiemann

Monad normalisation
by Joshua Schneider, Manuel Eberl and Andreas Lochbihler

Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals
by Jasmin Christian Blanchette, Mathias Fleury and Dmitriy Traytel

Formalization of Knuth–Bendix Orders for Lambda-Free Higher-Order Terms
by Heiko Becker, Jasmin Christian Blanchette, Uwe Waldmann and Daniel Wand

Formalization of Recursive Path Orders for Lambda-Free Higher-Order Terms
by Jasmin Christian Blanchette, Uwe Waldmann and Daniel Wand

The Z Property
by Bertram Felgenhauer, Julian Nagele, Vincent van Oostrom and Christian Sternagel

Decreasing Diagrams II
by Bertram Felgenhauer

Decreasing Diagrams
by Harald Zankl

Abstract Rewriting
by Christian Sternagel and René Thiemann