@misc{indiciaef80ccca053e3,
  title = {Formally Verified Native Code Generation in an Effectful JIT -- or: Turning the CompCert Backend into a Formally Verified JIT Compiler},
  author = {Aurèle Barrière and Sandrine Blazy and David Pichardie},
  year = {2022},
  doi = {10.1145/3571202},
  url = {https://arxiv.org/abs/2212.03129},
  note = {Source identifier: 2212.03129}
}