Type safety of rewrite rules in dependent types

TL;DR

This paper introduces a new method using Knuth-Bendix completion to ensure that user-defined rewriting rules in dependent type theory preserve typing, maintaining system consistency and decidability.

Contribution

It presents a novel approach to verify the type-preserving property of rewrite rules in dependent types using Knuth-Bendix completion.

Findings

The method effectively checks type preservation of rewriting rules.

It helps maintain decidability and logical consistency in dependent type systems.

The approach is applicable to extending type theory expressiveness safely.

Abstract

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.