Modeling Permutations in Coq for Coccinelle

Rewriting, Computation and Proof, pp. 259-269, 2007.

Cited by: 12|Bibtex|Views0|Links
EI
Keywords:
permut rfine grained modularitylist permutationsimple inductive definitionmodeling permutationsMore(6+)

Abstract:

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

Code:

Data:

Your rating :
0

 

Tags
Comments