This paper is difficult to follow. The pseudocode in particular contains errors. For example, the insert function looks at left.key and right.key without regard to whether left and right, respectively, are leaves and thus have keys. And insert calls itself recursively with the wrong number of arguments.

It seems to me that the interesting part of the paper is the claim of history independence. If I understand correctly, the basic idea is that, for a given set of keys and values, there exists only one possible tree. If that’s the intent, there should be a proof and probably a description of what the tree is for a given set of keys. If that’s not the intent, then a proof that the membership algorithm actually works is needed.