Bas Spitters (Aug 06 2020 at 09:16): Bas Spitters (Aug 06 2020 at 09:16):I stumbled on MLcompcert which connects miniml with compcert. Sort of like cakeml, but for Coq. I'm surprised I didn't hear about this before.
Does anyone know more about the project?
http://pauillac.inria.fr/~dargaye/mlcompcert.html
Karl Palmskog (Aug 06 2020 at 09:18):I remember looking at documentation/papers, but I don't think the "pure" source was ever released
Last updated: Sep 15 2024 at 12:01 UTC