Past Meetup

Typed Self-Evaluation via Intensional Type Functions, Brown&Palsberg -Érdi Gergő

This Meetup is past

5 people went

Location image of event venue


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?


This meetup is co-organized with BP Functional Programming Group ( and Budapest Haskell User Group ( and hosted/sponsored by EPAM.