论文标题
在依赖类型中类型重写规则的安全性
Type safety of rewrite rules in dependent types
论文作者
论文摘要
依赖类型理论的表现力可以通过识别类型模拟一些其他计算规则来扩展。但是，为了保留类型检查或系统逻辑一致性的可决定性，必须确保那些用户定义的重写规则保留键入。在本文中，我们提供了一种新方法，使用Knuth-Bendix完成检查该属性。
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.
