CFML 2.0 for CakeML

[myreen]

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

Here are a few URLs:

• his course on separation logic
• his construction of wpgen
• the script for a demo
• the last 2 pages of this paper explain the new xsimpl tactic

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]

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