Yann Leray, Gaëtan Gilbert, Nicolas Tabareau, Théo Winterhalter. The Rewster: Type Preserving Rewrite Rules for the Coq Proof Assistant. In Yves Bertot, Temur Kutsia, Michael Norrish, editors, 15th International Conference on Interactive Theorem Proving, ITP 2024, September 9-14, 2024, Tbilisi, Georgia. Volume 309 of LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. [doi]
Abstract is missing.