@zyang Cool stuff! - This paper is about NbE with term sharing: https://arxiv.org/pdf/2603.21949 Based on this, I attempted a simple Haskell implementation: https://gist.github.com/AndrasKovacs/0e1bc2532e071cef5974ca582f8090ad I'm not completely sure about the correctness of my version, but in the case it's wrong it would be fixed by using global "gensym", like in the paper. - This paper uses a similar evaluator, but since it's a conversion checker, it's quite a bit more complicated: https://hal.science/hal-05322705/document - Another direction of NbE optimization is to reduce space usage by "trimming" environments; this is well-known in closed evaluators but it's been used in normalizers too, e.g. in https://depositonce.tu-berlin.de/items/512ba4cd-ff0c-4f33-a5c2-a8fdc66dc03c and probably in the Rocq VM (not sure).