Formally Verified Native Code Generation in an Effectful JIT: Turning the CompCert Backend into a Formally Verified JIT Compiler

Aurèle Barrière, Sandrine Blazy, David Pichardie. Formally Verified Native Code Generation in an Effectful JIT: Turning the CompCert Backend into a Formally Verified JIT Compiler. Proceedings of the ACM on Programming Languages, 7(POPL):249-277, January 2023. [doi]

Abstract

Abstract is missing.