I'm sure the details are different, but the general idea, to me, seems the same as the one descibed by Leo and Sebastian in https://arxiv.org/abs/1908.05647 htt

I'm sure the details are different, but the general idea, to me, seems the same as the one descibed by Leo and Sebastian in https://arxiv.org/abs/1908.05647 https://arxiv.org/abs/1908.05647. Both Koka and Lean 4 use reference counting to know if it's safe to reuse a structure. This paper (Daan is a collegue of Leo at MS Research) gives a different formalization and proofs. The file is still named "fbip.pdf" though :)