Modular SMT Proofs for Fast Reflexive Checking Inside Coq
No abstract available.
DOI 10.1007/978-3-642-25379-9_13
Related papers
- A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses CPP 2011
- Rocket-Fast Proof Checking for SMT Solvers TACAS 2008
- Type Inference Logics OOPSLA 2024
- SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq TOPLAS 2023
- Safe, fast, concurrent proof checking for the lambda-pi calculus modulo rewriting CPP 2022
- Carcara: An Efficient Proof Checker and Elaborator for SMT Proofs in the Alethe Format TACAS 2023
- Fast Ramsey Quantifier Elimination in LIRA (with applications to liveness checking) TACAS 2026
- VeriML: typed computation of logical terms inside a language with effects ICFP 2010