A Safe Low-Level Language for Computer Algebra and Its Formally Verified Compiler. - Guillaume Melquiond; Josué Moreau (Proc. ACM Program. Lang., 2024)