TY  - RPRT
TI  - Formally Verified Native Code Generation in an Effectful JIT -- or: Turning the CompCert Backend into a Formally Verified JIT Compiler
AU  - Aurèle Barrière
AU  - Sandrine Blazy
AU  - David Pichardie
PY  - 2022
DO  - 10.1145/3571202
UR  - https://arxiv.org/abs/2212.03129
ID  - 2212.03129
ER  -