ACL2 version of the semantics of CakeML

[myreen]

Several people have contacted us asking to have the CakeML semantics in provers other than HOL4. There is an AFP entry with the CakeML semantics ported to Isabelle/HOL via Lem. However, people have also requested to have the semantics in ACL2 and Coq.

This issue is about producing a clean port for the ACL2 proof assistant.

There are two parts to this: (1) writing the definition in ACL2 in an idiomatic and nice way, and more importantly (2) engineering some way of automatically producing some evidence that the new formulation in ACL2 is accurate w.r.t. the HOL4 definitions that are used in the compiler proofs. Ideally, (2) should be able to detect and automatically flag discrepancies that need fixing in the ACL2 version when the CakeML semantics in HOL4 is updated.

I suggest that (2) is based on different forms of automatic testing. I believe this could be a nice topic for a Masters thesis, or a warm-up project for someone joining CakeML with a background in ACL2.

[tanyongkiam]

@myreen says this requires someone with expertise in ACL2.