Thursday 25 July 2019, 09:30, LSV library: Efficient pattern-matching in Dedukti, Gabriel Hondet (M2 intern, ENAC).

Lambdapi is a proof checker and a proof assistant using the lambdaPi calculus extended with rewrite rules. An efficient rewriting engine is mandatory to check proofs quickly. We will describe an efficient procedure for pattern matching based on the work of Luc Maranget implemented in the OCaml language and using decision trees. Our implementation show that our algorithm is in general better than a naive matching and in some cases, the complexity of matching can be reduced, thus improving drastically the performance.