Proof Abstraction for Imperative Languages
No abstract available.
DOI 10.1007/11924661_6
Related papers
- Velvet: A Foundational Multi-modal Verifier for Imperative Programs in Lean CAV 2026
- Quantified types in an imperative language TOPLAS 2006
- Compilation and Equivalence of Imperative Objects JFP 1999
- Effective interactive proofs for higher-order imperative programs ICFP 2009
- An integrated proof language for imperative programs PLDI 2009
- Efficient Verification of Imperative Programs Using Auto2 TACAS 2018
- A Provably Correct Compiler Generator ESOP 1992
- Imperative functional programs that explain their work ICFP 2017