Extensible and Efficient Automation Through Reflective Tactics

DOI10.1007/978-3-662-49498-1_21zbMath1335.68234OpenAlexW2478126725MaRDI QIDQ2802496

Jesper Bengtson, Gregory Malecha

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

Mathematics Subject Classification ID

Related Items (2)

The \textsc{MetaCoq} project ⋮ Constructive Galois Connections

Uses Software

• Coq
• Nuprl
• Toolchain
• Agda
• Mtac
• VeriML
• seL4
• Fiat
• Charge!
• Gallina

Cites Work

• Unnamed Item
• Unnamed Item
• Type Theory Should Eat Itself
• Fiat
• Compositional Computational Reflection
• Charge!
• Auto in Agda
• Proof-Producing Reflection for HOL
• A compiled implementation of strong reduction
• Verifying Object-Oriented Programs with Higher-Order Separation Logic in Coq
• A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
• Modular SMT Proofs for Fast Reflexive Checking Inside Coq
• Tactics for Reasoning Modulo AC in Coq
• Simple Types in Type Theory: Deep and Shallow Encodings
• Modular development of certified program verifiers with a proof assistant,
• Fast Reflexive Arithmetic Tactics the Linear Case and Beyond
• A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family
• VeriML
• How to make ad hoc proof automation less ad hoc
• Typed syntactic meta-programming
• Mtac
• Toward a verified relational database management system
• Lightweight Proof by Reflection Using a Posteriori Simulation of Effectful Computation
• Formal certification of a compiler back-end or
• Program Logics for Certified Compilers
• Importing HOL Light into Coq

This page was built for publication: Extensible and Efficient Automation Through Reflective Tactics