The paper on dynamic rebinding with Peter, Mike, Gareth and Keith has finally appeared in Journal of Functional Programming (here). [You may or may not be able to view it for free from the JFP page - depends where you're reading it from.]
This is a great relief! Contained within are details of Gareth's mega-theorem (which proves equivalence between CBV lambda-calculus and our funky late-binding calculi (lambda-r and lambda-d)). Gareth sweated blood over these!