Extensible and efficient automation through reflective tactics
From MaRDI portal
Publication:2802496
Recommendations
Cites work
- scientific article; zbMATH DE number 1088050 (Why is no real title available?)
- A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family
- A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
- A compiled implementation of strong reduction
- 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
- Importing HOL Light into Coq
- Lightweight proof by reflection using a posteriori simulation of effectful computation
- Modular SMT proofs for fast reflexive checking inside Coq
- Modular development of certified program verifiers with a proof assistant,
- 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
- VeriML: typed computation of logical terms inside a language with effects
- Verifying object-oriented programs with higher-order separation logic in Coq
Cited in
(23)- Improving the Usability of HOL Through Controlled Automation Tactics
- Constructive Galois connections
- The \textsc{MetaCoq} project
- How to make ad hoc proof automation less ad hoc
- Automated Deduction – CADE-20
- Compositional computational reflection
- Auto in Agda. Programming proof search using reflection
- Reflection of formal tactics in a deductive reflection framework
- Static and user-extensible proof checking
- Automatically proving equivalence by type-safe reflection
- Towards a scalable proof engine: a performant Prototype rewriting primitive for Coq
- Theorem Proving in Higher Order Logics
- Reification by parametricity -- fast setup for proof by reflection, in two lines of \textsc{Ltac}
- Mtac: a monad for typed tactic programming in Coq
- A Why3 framework for reflection proofs and its application to GMP's algorithms
- Definitional Quantifiers Realise Semantic Reasoning for Proof by Induction
- Meta-F\textsuperscript{\(\star\)}: proof automation with SMT, tactics, and metaprograms
- Lightweight proof by reflection using a posteriori simulation of effectful computation
- On Automation of OTS/CafeOBJ Method
- VeriML: typed computation of logical terms inside a language with effects
- Mtac: a monad for typed tactic programming in Coq
- Fast Reflexive Arithmetic Tactics the Linear Case and Beyond
- Practical reflection for sequent logics
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)
