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

https://hal.inria.fr/hal-02981528
Contributor : Frédéric Blanqui Connect in order to contact the contributor
Submitted on : Wednesday, October 28, 2020 - 9:25:42 AM
Last modification on : Wednesday, November 3, 2021 - 6:33:21 AM
Long-term archiving on: : Friday, January 29, 2021 - 6:13:12 PM

Files

fscd20.pdf
Files produced by the author(s)

Identifiers

Citation

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

Share

Metrics

Record views

46

Files downloads

321