Proof by computation in the Coq system

DOI10.1016/S0304-3975(00)00354-6zbMath0984.68137MaRDI QIDQ5958299

Martijn Oostdijk, Herman Geuvers

Publication date: 3 March 2002

Published in: Theoretical Computer Science (Search for Journal in Brave)

zbMATH Keywords

type theoryautomated proof development system

Mathematics Subject Classification ID

Related Items

Dealing with algebraic expressions over a field in Coq using Maple, Incorporating quotation and evaluation into Church's type theory, Proof by computation in the Coq system, A Logical Framework with Explicit Conversions

Uses Software

• Coq
• Automath
• LEGO

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Autarkic computations in formal proofs
• A two-level approach towards lean proof-checking
• Proof by computation in the Coq system