The example somehow reminds me of proof carrying code. If you obtain memory in pcc, you also get a proof that the memory is valid. If you want to use the memory, you need to pass the proof as well. Finally, the proof must be disposed and the only function that can do that for memory is free. This can be done for the reminder example as well.