Modeling Permutations in Coqfor Coccinelle

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

Cited by: 11|Bibtex|Views0|Links
EI

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 defi...More

Code:

Data:

Your rating :
0

 

Tags
Comments