Skip to Main content Skip to Navigation
Conference papers

Type safety of rewrite rules in dependent types

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.
Complete list of metadatas

https://hal.inria.fr/hal-02981528
Contributor : Frédéric Blanqui <>
Submitted on : Wednesday, October 28, 2020 - 9:25:42 AM
Last modification on : Wednesday, November 4, 2020 - 3:35:03 AM

Files

fscd20.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Frédéric Blanqui. Type safety of rewrite rules in dependent types. 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020), Jun 2020, Paris, France. pp.14, ⟨10.4230/LIPIcs.FSCD.2020.13⟩. ⟨hal-02981528⟩

Share

Metrics

Record views

19

Files downloads

58