The Rewster: Type Preserving Rewrite Rules for the Coq Proof Assistant.

Yann Leray, Gatan Gilbert, Nicolas Tabareau, Tho Winterhalter

Browse the full ITP paper archive.