Skip to Main content Skip to Navigation
New interface
Conference papers

The New Rewriting Engine of Dedukti

Abstract : 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. It thereforecontains an engine for rewriting LF terms and types according to the rewrite rules given by the user.A key component of this engine is the matching algorithm to find which rules can be fired. In thispaper, we describe the class of rewrite rules supported by Dedukti and the new implementation ofthe matching algorithm. Dedukti supports non-linear rewrite rules on terms with binders usinghigher-order pattern-matching as in Combinatory Reduction Systems (CRS). The new matchingalgorithm extends the technique of decision trees introduced by Luc Maranget in the OCamlcompiler to this more general context.
Complete list of metadata

https://hal.inria.fr/hal-02981561
Contributor : Gabriel Hondet Connect in order to contact the contributor
Submitted on : Friday, November 5, 2021 - 4:03:42 PM
Last modification on : Friday, August 5, 2022 - 2:58:08 PM

Files

fscd20.pdf
Publisher files allowed on an open archive

Identifiers

Citation

Gabriel Hondet, Frédéric Blanqui. The New Rewriting Engine of Dedukti. FSCD 2020 - 5th International Conference on Formal Structures for Computation and Deduction, Jun 2020, Paris, France. pp.16, ⟨10.4230/LIPIcs.FSCD.2020.35⟩. ⟨hal-02981561v2⟩

Share

Metrics

Record views

99

Files downloads

229