Certified Compilers à la Carte. - Oghenevwogaga Ebresafe; Ian Zhao; Ende Jin; Arthur Bright; Charles Jian; Yizhou Zhang 001 (Proc. ACM Program. Lang., 2025)