Inductive consequences in the calculus of constructions

DOI10.1007/978-3-642-14052-5_31MaRDI QIDQ5747669zbMATH OpenOpenAlexFDO

Authors Daria Walukiewicz-Chrząszcz, Jacek Chrząszcz

Publication date 14 September 2010

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-14052-5_31

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
• Definitions by rewriting in the Calculus of Constructions
• Termination of rewriting in the Calculus of Constructions
• Building Decision Procedures in the Calculus of Inductive Constructions

Cited in

(14)

• Induction, constructivity, and grounding
• Reduction and conversion strategies for the calculus of (co)inductive constructions. I
• A bi-directional refinement algorithm for the calculus of (co)inductive constructions
• scientific article; zbMATH DE number 4164162 (Why is no real title available?)
• scientific article; zbMATH DE number 4166886 (Why is no real title available?)
• Building Decision Procedures in the Calculus of Inductive Constructions
• Towards Rewriting in Coq
• scientific article; zbMATH DE number 4074451 (Why is no real title available?)
• An induction principle for consequence in arithmetic universes
• Definitions by rewriting in the Calculus of Constructions
• Theorem Proving in Higher Order Logics
• 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

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Inductive consequences in the calculus of constructions

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