Mtac: a monad for typed tactic programming in Coq
From MaRDI portal
Publication:5371944
Recommendations
Cites work
- A compact kernel for the calculus of inductive constructions
- A compiled implementation of strong reduction
- A framework for defining logics
- A machine-checked proof of the odd order theorem
- A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions
- Adjustable References
- Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
- CompCertTSO
- Compositional computational reflection
- Contextual modal type theory
- Extending Coq with Imperative Features and Its Application to SAT Verification
- First-Class Type Classes
- Formal proof - the four color theorem
- Hoare type theory, polymorphism and separation
- How to make ad hoc proof automation less ad hoc
- scientific article; zbMATH DE number 432706 (Why is no real title available?)
- scientific article; zbMATH DE number 1341617 (Why is no real title available?)
- scientific article; zbMATH DE number 6296049 (Why is no real title available?)
- Inductive types and type constraints in the second-order lambda calculus
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Lightweight proof by reflection using a posteriori simulation of effectful computation
- Mathematical Knowledge Management
- Meta-programming with names and necessity
- Mtac: a monad for typed tactic programming in Coq
- Programming with binders and indexed data-types
- Proof-assistants using dependent type systems
- Static and user-extensible proof checking
- Structuring the verification of heap-manipulating programs
- Subset Coercions in Coq
- Synthesis of distributed mobile programs using monadic types in Coq
- The power of parameterization in coinductive proof
- Typed Lambda Calculi and Applications
- Typed syntactic meta-programming
- VeriML: typed computation of logical terms inside a language with effects
- Ynot: dependent types for imperative programs
Cited in
(18)- Hammer for Coq: automation for dependent type theory
- Towards certified meta-programming with typed Template-Coq
- Reification by parametricity -- fast setup for proof by reflection, in two lines of \textsc{Ltac}
- Harpoon: mechanizing metatheory interactively
- The \textsc{MetaCoq} project
- scientific article; zbMATH DE number 1696760 (Why is no real title available?)
- Extensible and efficient automation through reflective tactics
- A proof dedicated meta-language
- Static and user-extensible proof checking
- An introduction to programming and proving with dependent types in Coq
- Coq Modulo Theory
- Beyond notations: hygienic macro expansion for theorem proving languages
- VeriML: typed computation of logical terms inside a language with effects
- Mtac: a monad for typed tactic programming in Coq
- A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading
- How to make ad hoc proof automation less ad hoc
- Meta-F\textsuperscript{\(\star\)}: proof automation with SMT, tactics, and metaprograms
- Towards automatic transformations of Coq proof scripts
This page was built for publication: Mtac: a monad for typed tactic programming in Coq
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5371944)
