Amend formalisation following the feedback from POPL21 artifact evaluation
In response to the concerns and suggestions from the POPL21 artifact evaluation team, we make the following changes:
-
The adequacy theorem receives a more direct statement in line with other Iris-based developments (the language
HeapLang
itself being such an example). The necessary amendments were all derived by one of the reviewers (Reviewer A). -
An implementation of
QueueLib
is added to the theory queue_lib.v. -
Minor corrections and enhancements to the README.md page and the scheduler.v theory are also performed.