Type safety of rewrite rules in dependent types, 14 pages, FSCD 2020, LIPIcs 167.

The expressiveness of dependent type theory can be extended by identifying types modulo some additional computation rules. But, for preserving the decidability of type-checking or the logical consistency of the system, one must make sure that those user-defined rewriting rules preserve typing. In this paper, we give a new method to check that property using Knuth-Bendix completion.

Statcounter W3C Validator Last updated on 21 January 2021. Come back to main page.