Modeling Permutations in Coq for Coccinelle

DOI10.1007/978-3-540-73147-4_13zbMATH Open1186.68429OpenAlexW1490766367MaRDI QIDQ3608821FDOQ3608821

Authors: Evelyne Contejean 

Publication date: 6 March 2009

Published in: Rewriting, Computation and Proof (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-73147-4_13

Recommendations

• Permutations in Coinductive Graph Representation
• General algorithms for permutations in equational inference
• Coq Modulo Theory
• Tactics for Reasoning Modulo AC in Coq
• All sorts of permutations (functional pearl)

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Cited In (2)

• Certifying a Termination Criterion Based on Graphs, without Graphs
• Coccinelle

Uses Software

• Coq
• CoLoR

This page was built for publication: Modeling Permutations in Coq for Coccinelle

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3608821)