A tactic language for the system Coq

DOI10.1007/3-540-44404-1_7MaRDI QIDQ2767010zbMATH OpenFDO

Authors David Delahaye

Publication date 22 July 2002

Published in Lecture Notes in Artificial Intelligence (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-44404-1_7

Mathematics Subject Classification ID

Recommendations

• A proof dedicated meta-language
• A tactic calculus. --- Abridged version
• Mtac: a monad for typed tactic programming in Coq
• Mtac: a monad for typed tactic programming in Coq
• A tactic language for Ergo

Cited in

(39)

• Towards certified meta-programming with typed Template-Coq
• A Coq tactic for equality learning in linear arithmetic
• Tactics and certificates in Meta Dedukti
• A tactic calculus. --- Abridged version
• TacticToe: learning to prove with tactics
• Harpoon: mechanizing metatheory interactively
• The Tactician. A seamless, interactive tactic learner and prover for Coq
• Crystal: Integrating structured queries into a tactic language
• A proof dedicated meta-language
• Eisbach: a proof method language for Isabelle
• Rewriting strategies and strategic rewrite programs
• Verifying B proof rules using deep embedding and automated theorem proving
• Automated Certification of Implicit Induction Proofs
• Hints in Unification
• Why Would You Trust B?
• A Declarative Language for the Coq Proof Assistant
• Proving Bounds on Real-Valued Functions with Computations
• A tactic language for Ergo
• Free-style theorem proving
• CtCoq: a system presentation
• Tactics and parameters
• Deep Generation of Coq Lemma Names Using Elaborated Terms
• Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages
• Beyond notations: hygienic macro expansion for theorem proving languages
• Mtac: a monad for typed tactic programming in Coq
• Handcrafted inversions made operational on operational semantics
• Mtac: a monad for typed tactic programming in Coq
• Experimenting Formal Proofs of Petri Nets Refinements
• A Tactic Language for Hiproofs
• Types for Proofs and Programs
• Trace-based verification of imperative programs with I/O
• Tactics for hierarchical proof
• Formal Verification of Bit-Vector Invertibility Conditions in Coq
• Structured monads for generic first-order syntax metatheory
• Towards automatic transformations of Coq proof scripts
• Syntax monads for the working formal metatheorist
• Pgeon: generating tableau-based provers from declarative specifications of logical calculi
• Tool-assisted specification and verification of typed low-level languages
• The proof monad

Describes a project that uses

Uses Software

• Coq
• PVS

This page was built for publication: A tactic language for the system Coq

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