Import OCPL's heap_lang logic?
From !37 (merged):
Please take a look at the heap interface in Fig. 2 of my OCPL paper (off my home page) or, more informatively, at theories/heap_lang/heap.v in the OCPL Coq development. I propose replacing the current heap_lang logic with the strictly more expressive OCPL, and adding the OCPL examples to heap_lang/lib and tests/.
Ralf asked if I have a git repo. Yes. I will create a merge request once we settle !37 (merged). (OCPL builds on !37 (merged).)