A code rewrite tool for structural search and replace that supports ~every language.

Proof assistant based on the λΠ-calculus modulo rewriting

An automatic theorem prover in OCaml for typed higher-order logic with equality and datatypes, based on superposition+rewriting; and Logtk, a supporting library for manipulating terms, formulas, clauses, etc.

[toy] A rewriting language similar to the core of Mathematica

A proof-producing SMT/McSat solver, handling polymorphic first-order logic, and using an SMT/McSat core extended using Tableaux, Superposition and Rewriting.

Algebraic structures in OCaml.

Hypergraph rewriting for PROPs

Homotopy and rewriting

Polygraphic rewriting

Rewrite system stats n' count