Towards Rewriting in Coq

DOI10.1007/978-3-540-73147-4_6zbMATH Open1186.68234OpenAlexW139065648MaRDI QIDQ3608814FDOQ3608814

Daria Walukiewicz-Chrząszcz, Jacek Chrząszcz

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_6

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Cited In (9)

• Importing HOL Light into Coq
• From Sets to Bits in Coq
• Title not available (Why is that?)
• Type Theory Unchained : Extending Agda with User-Defined Rewrite Rules
• Title not available (Why is that?)
• Nested abstract syntax in Coq
• Title not available (Why is that?)
• Encoding natural semantics in Coq
• Types for Proofs and Programs

Uses Software

• Coq
• CiME

   Recommendations

• Consistency and Completeness of Rewriting in the Calculus of Constructions 👍 👎
• Consistency and Completeness of Rewriting in the Calculus of Constructions 👍 👎
• Tactics for Reasoning Modulo AC in Coq 👍 👎
• A new look at generalized rewriting in type theory 👍 👎
• Inductive consequences in the calculus of constructions 👍 👎

This page was built for publication: Towards Rewriting in Coq

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