Extensible Proof-Producing Compilation
No abstract available.
Related papers
- Relational compilation for performance-critical applications: extensible proof-producing translation of functional models into low-level code PLDI 2022
- Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic ESOP 2007
- Fully abstract module compilation POPL 2019
- A Verified Compiler from Isabelle/HOL to CakeML ESOP 2018
- Bringing extensibility to verified compilers PLDI 2010
- Static and user-extensible proof checking POPL 2012
- Generating compiler optimizations from proofs POPL 2010
- Compiling for automatically generated instruction set extensions CGO 2012