%0 Journal Article %1 journals/pacmpl/BarriereBP23 %A Barrière, Aurèle %A Blazy, Sandrine %A Pichardie, David %D 2023 %J Proc. ACM Program. Lang. %K dblp %N POPL %P 249-277 %T Formally Verified Native Code Generation in an Effectful JIT: Turning the CompCert Backend into a Formally Verified JIT Compiler. %U http://dblp.uni-trier.de/db/journals/pacmpl/pacmpl7.html#BarriereBP23 %V 7

@article{journals/pacmpl/BarriereBP23, added-at = {2023-10-22T00:00:00.000+0200}, author = {Barrière, Aurèle and Blazy, Sandrine and Pichardie, David}, biburl = {https://www.bibsonomy.org/bibtex/20940b05c3d442155bdaaf39f8bfea2c5/dblp}, ee = {https://www.wikidata.org/entity/Q122926283}, interhash = {7a7da096a29da72823446c06086a0089}, intrahash = {0940b05c3d442155bdaaf39f8bfea2c5}, journal = {Proc. ACM Program. Lang.}, keywords = {dblp}, month = {January}, number = {POPL}, pages = {249-277}, timestamp = {2024-04-08T09:54:45.000+0200}, title = {Formally Verified Native Code Generation in an Effectful JIT: Turning the CompCert Backend into a Formally Verified JIT Compiler.}, url = {http://dblp.uni-trier.de/db/journals/pacmpl/pacmpl7.html#BarriereBP23}, volume = 7, year = 2023 }