@article{barriere:hal-03882598,
TITLE = {Formally Verified Native Code Generation in an Effectful JIT - or: Turning the CompCert Backend into a Formally Verified JIT Compiler},
AUTHOR = {Barri{\`e}re, Aur{\`e}le and Blazy, Sandrine and Pichardie, David},
URL = {https://inria.hal.science/hal-03882598},
JOURNAL = {Proceedings of the ACM on Programming Languages},
PUBLISHER = {ACM},
VOLUME = {7},
NUMBER = {POPL},
PAGES = {249-277},
YEAR = {2023},
MONTH = Jan, DOI = {10.1145/3571202},
KEYWORDS = {verified compilation ; just-in-time compilation ; CompCert compiler},
PDF = {https://inria.hal.science/hal-03882598/file/main.pdf},
HAL_ID = {hal-03882598},
HAL_VERSION = {v1},
}