Extensible and Efficient Automation Through Reflective Tactics
From MaRDI portal
Publication:2802496
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
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (2)
Uses Software
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
