From Rewrite Rules to Axioms in the $\lambda$$\Pi$-Calculus Modulo Theory
<|reference_start|>From Rewrite Rules to Axioms in the $\lambda$$\Pi$-Calculus Modulo Theory: 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 rewrite rules of a theory of the $\lambda$$\Pi$-calculus modulo theory by equational axioms, when this theory features the notions of proposition and proof, while maintaining the same expressiveness. To do so, we introduce in the target theory a heterogeneous equality, and we build a translation that replaces each use of the conversion rule by the insertion of a transport. At the end, the theory with rewrite rules is a conservative extension of the theory with axioms.<|reference_end|>
@article{blot2024from,
    title={From Rewrite Rules to Axioms in the $\lambda$$\Pi$-Calculus Modulo
  Theory},
    author={Valentin Blot (DEDUCTEAM, LMF, ENS Paris Saclay), Gilles Dowek
  (DEDUCTEAM, LMF, ENS Paris Saclay), Thomas Traversi'e (DEDUCTEAM, LMF, ENS
  Paris Saclay, MICS), Th'eo Winterhalter (DEDUCTEAM, LMF, ENS Paris Saclay)},
    journal={arXiv preprint arXiv:2402.09024},
    year={2024},
    archivePrefix={arXiv},
    eprint={2402.09024},
    primaryClass={cs.LO}
}