65 citations · 211 across the 36 of their papers we have counts for
Showing 2020Show all
2 papers · 1 filter
cs.LO2020★ 2 cited
Type safety of rewrite rules in dependent types
Frédéric Blanqui
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…
cs.PL2020★ 10 cited
The New Rewriting Engine of Dedukti
Gabriel Hondet, Frédéric Blanqui
Dedukti is a type-checker for the -calculus modulo rewriting, an extension of Edinburgh's logicalframework LF where functions and type symbols can be defined by rewrite rules…