search

CakeML / cakeml

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

CFML 2.0 for CakeML #813

Open myreen opened 3 years ago

myreen commented 3 years ago

Arthur Charguéraud has developed a new version of CFML based on weakest preconditions.

Here are a few URLs:

This new version seems slicker than the CF definitions and automation used in CakeML's version of CF, which are based on Charguéraud's previous version of CFML.

This issue is about developing a CakeML version of Charguéraud's new CFML.

It would be good if the new CF for CakeML would be compatible with the current CF for CakeML. In particular, it would be good if app theorems proved in one are equivalent to app theorems proved in the other.

charguer commented 3 years ago

Happy to help out by explaining how things work in details to whoever is interested to hack this stuff in CakeML.