Verifying Low-Level Implementations of High-Level Datatypes
Abstract elided by the publisher.
Related papers
- High-level views on low-level representations ICFP 2005
- Verified low-level programming embedded in F ICFP 2017
- Verifying Custom Synchronization Constructs Using Higher-Order Separation Logic TOPLAS 2016
- Verified Lock-Free Session Channels with Linking OOPSLA 2024
- LMS-Verify: abstraction without regret for verified systems programming POPL 2017
- Verified tensor-program optimization via high-level scheduling rewrites POPL 2022
- Modularity, Code Specialization, and Zero-Cost Abstractions for Program Verification ICFP 2023
- Tabby: A Synthesis-Aided Compiler for High-Performance Zero-Knowledge Proof Circuits OOPSLA 2025