Automated Resource Analysis with Coq Proof Objects
No abstract available.
DOI 10.1007/978-3-319-63390-9_4
Related papers
- Liquid resource types ICFP 2020
- ATLAS: Automated Amortised Complexity Analysis of Self-adjusting Data Structures CAV 2021
- How to make ad hoc proof automation less ad hoc JFP 2013
- Practical Tactics for Verifying C Programs in Coq CPP 2015
- Mtac: a monad for typed tactic programming in Coq ICFP 2013
- Mostly Automated Proof Repair for Verified Libraries PLDI 2023
- A mechanized semantics for C++ object construction and destruction, with applications to resource management POPL 2012
- Automating formal proofs for reactive systems PLDI 2014