Modeling Permutations in Coq for Coccinelle

DOI10.1007/978-3-540-73147-4_13MaRDI QIDQ3608821zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

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)

Cited in

(2)

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

Describes a project that uses

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)