Isabelle/HOL mechanisation of our IPL 2017 submission: "The Interchange Law: A Principle of Concurrent Programming".

Authors: Tony Hoare, Bernhard Möller, Georg Struth, and Frank Zeyda.

The accompanying report is provided by the report.pdf document. The Isabelle theories are in the "theories" folder. In order to load them, please add the repository root directory to the ROOTS file of the Isabelle installation and select the HOL-Eisbach heap e.g. in jedit. The ICL heap can be build (under Linux) with the included build.sh script.

For any queries related to the mechanisation please email: [email protected].