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

• A tactic language for the system Coq
• Mtac: a monad for typed tactic programming in Coq
• Mtac: a monad for typed tactic programming in Coq
• Tactics and certificates in Meta Dedukti
• Two-level meta-reasoning in Coq

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
• A metalanguage for programming with bound names modulo renaming
• A tactic language for the system Coq
• A Declarative Language for the Coq Proof Assistant
• A metalanguage for guarded iteration

Describes a project that uses

Uses Software

• Coq
• Camlp4
• ML
• OCaml
• LCF

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)