Extensible and efficient automation through reflective tactics
From MaRDI portal
Recommendations
Cites work
- A compiled implementation of strong reduction
- A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family
- A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
- Auto in Agda. Programming proof search using reflection
- Charge! A framework for higher-order separation logic in Coq
- Compositional computational reflection
- Fast Reflexive Arithmetic Tactics the Linear Case and Beyond
- Fiat: deductive synthesis of abstract data types in a proof assistant
- Formal certification of a compiler back-end or: programming a compiler with a proof assistant
- How to make ad hoc proof automation less ad hoc
- scientific article; zbMATH DE number 1088050 (Why is no real title available?)
- Importing HOL Light into Coq
- Lightweight proof by reflection using a posteriori simulation of effectful computation
- Modular development of certified program verifiers with a proof assistant,
- Modular SMT proofs for fast reflexive checking inside Coq
- Mtac: a monad for typed tactic programming in Coq
- Program logics for certified compilers
- Proof-producing reflection for HOL. With an application to model polymorphism
- Sets in Coq, Coq in Sets
- Simple Types in Type Theory: Deep and Shallow Encodings
- Tactics for Reasoning Modulo AC in Coq
- Toward a verified relational database management system
- Type theory should eat itself
- Typed syntactic meta-programming
- Verifying object-oriented programs with higher-order separation logic in Coq
- VeriML: typed computation of logical terms inside a language with effects
Cited in
(23)- Reification by parametricity -- fast setup for proof by reflection, in two lines of \textsc{Ltac}
- A Why3 framework for reflection proofs and its application to GMP's algorithms
- The \textsc{MetaCoq} project
- Automatically proving equivalence by type-safe reflection
- Practical reflection for sequent logics
- Compositional computational reflection
- Auto in Agda. Programming proof search using reflection
- Static and user-extensible proof checking
- Improving the Usability of HOL Through Controlled Automation Tactics
- Fast Reflexive Arithmetic Tactics the Linear Case and Beyond
- Reflection of formal tactics in a deductive reflection framework
- Constructive Galois connections
- VeriML: typed computation of logical terms inside a language with effects
- Mtac: a monad for typed tactic programming in Coq
- Lightweight proof by reflection using a posteriori simulation of effectful computation
- Mtac: a monad for typed tactic programming in Coq
- Automated Deduction – CADE-20
- How to make ad hoc proof automation less ad hoc
- On Automation of OTS/CafeOBJ Method
- Theorem Proving in Higher Order Logics
- Meta-F\textsuperscript{\(\star\)}: proof automation with SMT, tactics, and metaprograms
- Definitional Quantifiers Realise Semantic Reasoning for Proof by Induction
- Towards a scalable proof engine: a performant Prototype rewriting primitive for Coq
This page was built for publication: Extensible and efficient automation through reflective tactics
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2802496)
