A Verified Efficient Implementation of the Weighted Path Order. - René Thiemann; Elias Wenninger (Arch. Formal Proofs, 2023)