Modeling Permutations in Coqfor Coccinelle
Rewriting Computation and Proof, pp. 259-269, 2007.
In this paper we present the part of the Coccinelle library which deals with list permutations. Indeed permutations naturally arise when formally modeling rewriting in Coq, for instance RPO with multiset status and equality modulo AC. Moreover the needed permutations are up to an equivalence relation, and may be used to inductively defi...More
Full Text (Upload PDF)
PPT (Upload PPT)