The New Rewriting Engine of Dedukti

Gabriel Hondet, Frédéric Blanqui

Dedukti is a type-checker for the $\lambda$$\Pi$-calculus modulo rewriting, an extension of Edinburgh's logicalframework LF where functions and type symbols can be defined by rewrite rules…