Towards Rewriting in Coq

DOI10.1007/978-3-540-73147-4_6MaRDI QIDQ3608814zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

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

Cited in

(15)

• Nested abstract syntax in Coq
• From Sets to Bits in Coq
• scientific article; zbMATH DE number 6678680 (Why is no real title available?)
• A new look at generalized rewriting in type theory
• scientific article; zbMATH DE number 2000441 (Why is no real title available?)
• Encoding natural semantics in Coq
• Types for Proofs and Programs
• Importing HOL Light into Coq
• scientific article; zbMATH DE number 7649963 (Why is no real title available?)
• Types for Proofs and Programs
• Consistency and Completeness of Rewriting in the Calculus of Constructions
• Proof search and proof check for equational and inductive theorems.
• Consistency and Completeness of Rewriting in the Calculus of Constructions
• Type Theory Unchained : Extending Agda with User-Defined Rewrite Rules
• An Isabelle/HOL formalization of semi-Thue and conditional semi-Thue systems

Describes a project that uses

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)