It's a nice write up but I'm not sure what the contribution is. I would have expected more engagement with Peter Van Roy's work, in particular his and Seif Haridi's epic book CTM [1] where the logic variable got properly unpacked more than 15 years previously. Or at least a citation.
Has anyone looked into how to decouple logic variables from backtracking? i.e., is there a good reason to unbind a variable apart from the Prolog discipline? (Without unbinding we get single-assignment variables where initialisation is decoupled from declaration, which I feel can often be simulated with laziness ala Haskell, but see CTM.)