Nested_Multisets_Ordinals Dependents
2021
Formalization of Timely Dataflow's Progress Tracking Protocol
by Matthias Brun, Sára Decova, Andrea Lattuada and Dmitriy Traytel
2020
2018
A Verified Functional Implementation of Bachmair and Ganzinger's Ordered Resolution Prover
by Anders Schlichtkrull, Jasmin Christian Blanchette and Dmitriy Traytel
Formalization of Bachmair and Ganzinger's Ordered Resolution Prover
by Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel and Uwe Waldmann
2016
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