Okay, so this is the second attempt to cook up a rusty borrow checker (note from the author, a few years later: which succeeded). The first time, I've devised it as a system separate from the type system, but to be honest, the type system should be more that sufficient to do borrow checking. Another requirement is that we need to do it during partial evaluation so that we can generate destructors at the appropriate moment.
The basic idea is to be able to mark values as unique, so that they may only be bound to a single parameter at a time. When a function with parameters bound to unique values goes out of scope, the values will be destroyed. If a value subsequently holds other unique values, those values will be destroyed along with it.
A value can be saved from destruction by either making it a child of another unique value, or binding it to the parameter of a return continuation.
Thus we observe that parameters can be alive or dead. A parameter is alive when it is first created, and dies when its value has been assigned to a different parameter. Any parameter still alive when the function returns will destroy its value. The liveness status of a parameter is recorded into the current frame, so that parameters are never mutated directly, and branches can see parameters in different stadium.
One has to wonder then what happens when a parameter dies in one branch, but is kept alive in another. It seems like the best course of action when merging branches, and one or more branches have spent a parameter, is for all branches where the parameter is still alive to run a special post block where the parameter is destroyed to ensure that the parameter is spent after both branches return.
We invent another status of values, which is that of a weakly referenced unique value (a "view"); a weak reference can only be taken in the same scope in which the parameter bound to the unique value is alive, and becomes invalid when the unique value is moved or destroyed.
Thus we observe that parameters can be borrowed. When a reference to an alive parameter is created, the parameter becomes borrowed. It is allowed to spend a borrowed parameter. Any borrowed reference to the parameter still alive when the parameter is spent, becomes inaccessible.