Towards Rewriting in Coq

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

Authors: Jacek Chrząszcz, Daria Walukiewicz-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

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

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Cited In (14)

• Importing HOL Light into Coq
• From Sets to Bits in Coq
• Proof search and proof check for equational and inductive theorems.
• Types for Proofs and Programs
• Consistency and Completeness of Rewriting in the Calculus of Constructions
• Consistency and Completeness of Rewriting in the Calculus of Constructions
• Title not available (Why is that?)
• Type Theory Unchained : Extending Agda with User-Defined Rewrite Rules
• Title not available (Why is that?)
• A new look at generalized rewriting in type theory
• 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

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)