From Rewrite Rules to Axioms in the $\hat{I}»$$\hat{I}$-Calculus Modulo Theory

Valentin Blot, Gilles Dowek, Thomas Traversié +1

The $\hat{I}»$$\hat{I}$-calculus modulo theory is an extension of simply typed $\hat{I}»$-calculus with dependent types and user-defined rewrite rules. We show that it is possible to replace the re…