Undecidability Results on Orienting Single Rewrite Rules by René Thiemann, Fabian Mitterwallner and Aart Middeldorp Apr 25
A Verified Efficient Implementation of the Weighted Path Order by René Thiemann and Elias Wenninger Jun 01
A Formalization of Weighted Path Orders and Recursive Path Orders by Christian Sternagel, René Thiemann and Akihisa Yamada Sep 16
Formalization of the Embedding Path Order for Lambda-Free Higher-Order Terms by Alexander Bentkamp Oct 19
Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals by Jasmin Christian Blanchette, Mathias Fleury and Dmitriy Traytel Nov 12
Formalization of Knuth–Bendix Orders for Lambda-Free Higher-Order Terms by Heiko Becker, Jasmin Christian Blanchette, Uwe Waldmann and Daniel Wand Nov 12
Formalization of Recursive Path Orders for Lambda-Free Higher-Order Terms by Jasmin Christian Blanchette, Uwe Waldmann and Daniel Wand Sep 23
The Z Property by Bertram Felgenhauer, Julian Nagele, Vincent van Oostrom and Christian Sternagel Jun 30