Separation Logic in Coq - News
17/01/06: module store extended with extensionality
Item posted by Reynald Affeldt <reynald> on Tue 17 Jan 2006 04:59:00 AM UTC.
This extension required a slight change of the module interface.
The core framework has been updated to cope with this change.
Topsy proofs are still temporarily broken.
Powered by Savane 3.14-50d9.
Corresponding source code