Idris[1] and most of the dependent typed languages that I've looked at use de Bruijn numbers. (As does my own[2].)

The Idris implementation also has a list of names in scope as an argument to the type of a Term, which makes the compiler (also Idris) check if you're making a mistake with your de Bruijn indices. (I did not do this in mine, but I should have.)

Edit: Oh, I see you mention reusing computations, that may be a bit more subtle. I'll have to look at your repo to see what you mean by that.

[1]: https://github.com/idris-lang/Idris2 [2]: https://github.com/dunhamsteve/newt