ICFP 2024 (series) / Artifact Evaluation /
A Safe Low-level Language for Computer Algebra and its Formally Verified Compiler
Our artifact extends the CompCert verified compiler with a new input language. Running it does not require more resources than what is needed for compiling and running CompCert, that is, mostly the Coq proof assistant.