[PRL] Type-directed partial evaluation

[Mitchell Wand]

> BTW, the situation corresponds to "sourcing" an optimized piece of
> code.

I'm not sure that's accurate, depending on what you mean by
"sourcing".

In TDPE the source is derived simply by _running_ the code in a
controlled fashion (on symbolic data, if I recall correctly).  It's
not a question of "decompiling from the byte code".

TDPE turns out to be a special case of something called "Normalization
by Evaluation" (NBE), which has been of interest in the LICS community
for some time.  The correctness proofs of all of these are quite subtle.

--Mitch