From Rewrite Rules to Axioms in the $\lambda$$\Pi$-Calculus Modulo Theory

Valentin Blot, Gilles Dowek, Thomas Traversié +1

The $\lambda$$\Pi$-calculus modulo theory is an extension of simply typed $\lambda$-calculus with dependent types and user-defined rewrite rules. We show that it is possible to replace the rewri…