search

CakeML / cakeml

CakeML: A Verified Implementation of ML
https://cakeml.org
Other
947 stars 83 forks source link

Target official ARM semantics #601

Open xrchz opened 5 years ago

xrchz commented 5 years ago

A version of the ARM ISA in Sail has been made available here. This model originates with ARM, so has some form of legitimacy. This issue is to add this model of ARM as a target for CakeML (possibly replacing one or more of our existing ARM targets).

myreen commented 5 years ago

Sounds good. A first step would be to get a HOL export from sail into HOL/examples.

AndreasLoow commented 5 years ago

Just to link the issues: The following issue is related to defining the very large records included in the current ARM model: HOL-Theorem-Prover/HOL#713. Currently, it takes over two hours to define the large records in the model.