Extensible and efficient automation through reflective tactics
From MaRDI portal
Publication:2802496
DOI10.1007/978-3-662-49498-1_21zbMATH Open1335.68234OpenAlexW2478126725MaRDI QIDQ2802496FDOQ2802496
Authors: Gregory Malecha, Jesper Bengtson 
Publication date: 26 April 2016
Published in: Programming Languages and Systems (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-662-49498-1_21
Recommendations
Cites Work
- VeriML: typed computation of logical terms inside a language with effects
- Mtac: a monad for typed tactic programming in Coq
- Fiat: deductive synthesis of abstract data types in a proof assistant
- Sets in Coq, Coq in Sets
- A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
- Simple Types in Type Theory: Deep and Shallow Encodings
- Formal certification of a compiler back-end or: programming a compiler with a proof assistant
- Toward a verified relational database management system
- Program logics for certified compilers
- Importing HOL Light into Coq
- A compiled implementation of strong reduction
- Title not available (Why is that?)
- Typed syntactic meta-programming
- Charge! A framework for higher-order separation logic in Coq
- Fast Reflexive Arithmetic Tactics the Linear Case and Beyond
- Verifying object-oriented programs with higher-order separation logic in Coq
- Lightweight proof by reflection using a posteriori simulation of effectful computation
- Tactics for Reasoning Modulo AC in Coq
- Modular SMT proofs for fast reflexive checking inside Coq
- Type theory should eat itself
- Compositional computational reflection
- Auto in Agda. Programming proof search using reflection
- A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family
- Proof-producing reflection for HOL. With an application to model polymorphism
- Modular development of certified program verifiers with a proof assistant,
- How to make ad hoc proof automation less ad hoc
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
- Towards a scalable proof engine: a performant Prototype rewriting primitive for Coq
- Automatically proving equivalence by type-safe reflection
- Theorem Proving in Higher Order Logics
- Mtac: a monad for typed tactic programming in Coq
- 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
- 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
Uses Software
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)
