Modeling Permutations in Coq for Coccinelle
Rewriting, Computation and Proof, pp. 259-269, 2007.
permut rfine grained modularitylist permutationsimple inductive definitionmodeling permutationsMore(6+)
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 define...More
Full Text (Upload PDF)
PPT (Upload PPT)