Gergő will be presenting Brown & Palsberg's paper from POPL 2017: "Typed Self-Evaluation via Intensional Type Functions".
We can easily make a typed representation for STLC in Haskell, and
then write an evaluator over that representation. But can we write
that in STLC? Or can we write it in Haskell, but for Haskell itself?
This paper is in some sense a sequel to last year's "Breaking Through
the Normalization Barrier" by the same authors; that one was about
self-unquoting of the form
unquote : Exp t -> t
This one is about self-reduction of the form
reduce : Exp t -> Exp t
(with the result encoding a normal form)
In both cases, the question we are interested in is, can we arrange
for the host and the target language to coincide?