| comparisons.  I really think the community needs a bunch
| of "systems" paper on this topic that do a careful examination 
| of the tradeoffs for important applications like type-checkers,
| compilers, and theorem provers.  Like realistic techniques
| for garbage collection, too much is locked in the brains of 
| implementors.

Indeed, if any participant of this discussion is so motivated, I would
dearly love to publish a paper about the practical aspects of
efficient management of substitution and bound variables in the
Journal of Functional Programming.  It doesn't have to be a "new idea".
Just articulating the unpublished experience and laying out design tradeoffs
that we've seen in this discussion would be excellent. 

Send me a paper!  (Or send it to Greg, who's also a JFP editor.)

Simon