A proof dedicated meta-language

MaRDI QIDQ2844812zbMATH OpenFDO

Authors David Delahaye

Publication date 19 August 2013

Full work available at URL http://www.sciencedirect.com/science/article/pii/S1571066104805085

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Logic in computer science (03B70)

Recommendations

• scientific article; zbMATH DE number 1696760
• Mtac: a monad for typed tactic programming in Coq
• Mtac: a monad for typed tactic programming in Coq
• Tactics and certificates in Meta Dedukti
• scientific article; zbMATH DE number 1927423

Cited in

(7)

• Metamath Zero: designing a theorem prover prover
• Automatically proving equivalence by type-safe reflection
• Crystal: Integrating structured queries into a tactic language
• scientific article; zbMATH DE number 1612495 (Why is no real title available?)
• scientific article; zbMATH DE number 1696760 (Why is no real title available?)
• A Declarative Language for the Coq Proof Assistant
• A metalanguage for guarded iteration

Describes a project that uses

Uses Software

• Coq
• ML
• OCaml
• LCF
• Camlp4

This page was built for publication: A proof dedicated meta-language

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