Type safety of rewrite rules in dependent types
Résumé
The expressiveness of dependent type theory can beextended by identifying types modulo some additional computation rules. But, forpreserving the decidability of type-checking or the logicalconsistency of the system, one must make sure that those user-definedrewriting rules preserve typing. In this paper, we give a newmethod to check that property using Knuth-Bendix completion.
Origine : Fichiers produits par l'(les) auteur(s)