Paper Info
Title
The New Rewriting Engine of Dedukti (System Description).
Abstract
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. 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.
Year
DOI
Venue
2020
10.4230/LIPIcs.FSCD.2020.35
FSCD
DocType
ISSN
Citations 
Conference
5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020), Jun 2020, Paris, France. pp.16
0
PageRank 
References 
Authors
0.34
0
2
Name
Order
Citations
PageRank
Gabriel Hondet101.01
Frédéric Blanqui212.04