@article{forster_etal_2024, title={Verified Extraction from Coq to OCaml}, volume={8}, ISSN={2475-1421}, url={http://dx.doi.org/10.1145/3656379}, DOI={10.1145/3656379}, number={PLDI}, journal={Proceedings of the ACM on Programming Languages}, publisher={Association for Computing Machinery (ACM)}, author={Forster, Yannick and Sozeau, Matthieu and Tabareau, Nicolas}, year={2024}, month=jun, pages={52–75} }