Proof-Directed De-compilation of Low-Level Code
Abstract elided by the publisher.
Related papers
- A provably sound TAL for back-end optimization PLDI 2003
- Relational compilation for performance-critical applications: extensible proof-producing translation of functional models into low-level code PLDI 2022
- A proof theory for machine code TOPLAS 2007
- The impact of optional type information on jit compilation of dynamically typed languages DLS 2011
- A Symbolic Emulator for Shuffle Synthesis on the NVIDIA PTX Code CC 2023
- Design and evaluation of dynamic optimizations for a Java just-in-time compiler TOPLAS 2005
- Biorthogonality, step-indexing and compiler correctness ICFP 2009
- Verified low-level programming embedded in F ICFP 2017