Theorems for Free from Separation Logic Specifications: ICFP'21 artifact
- Birkedal, Lars
- Dinsdale-Young, Thomas
- Guéneau, Armaël
- Jaber, Guilhem
- Svendsen, Kasper
- Tzevelekos, Nikos
Publication date
May 2021
DOIAbstract
This upload contains the Coq formalization associated with the ICFP'21 paper "Theorems for Free from Separation Logic Specifications". It provides both a zip archive with the source code for the Coq proofs, as well as a QEmu VM image allowing to easily run Coq to proof-check the scripts. See the README.md file for more information
Add to ORKG