Bottom-up rewriting with smart constructors, hereditary substitution & normalization by evaluation: julesjacobs.com/notes/smartcon
Conversation
Is your definition of NbE a bit more narrow than mine? I use a closure-converted form, for example, with De Bruijn levels in neutral values. I've also seen strings used in place of levels in other implementations of NbE.
3
2
I dunno if this is related at all? 🤔
Quote Tweet
Almost like NbE is a bit like 'lazy closure conversion + partial evaluation' perhaps…?
I'm pretty bad at theory stuff, so it's likely I'm wrong about this, misunderstanding, or that you are already aware! Just thought I'd mention it in case it's of any use! 
Show this thread
Replying to
I think normalization under lamdbas is related to partial evaluation, and furthermore typed NbE seems indeed related to type directed partial evaluation. I'd also like to know what the exact correspondence is, let me know if you find out!
1
1
Alas, it's not likely I'll be able to find out with more confidence than ‘huh, that seems funny and possibly related…’ Very thankful to those who know how to do the hard work of actually formalising things properly. But if I miraculously conjure up a proof I'll let you know!