addressalign-toparrow-leftarrow-rightbackbellblockcalendarcameraccwcheckchevron-downchevron-leftchevron-rightchevron-small-downchevron-small-leftchevron-small-rightchevron-small-upchevron-upcircle-with-checkcircle-with-crosscircle-with-pluscrossdots-three-verticaleditemptyheartexporteye-with-lineeyefacebookfolderfullheartglobegmailgooglegroupshelp-with-circleimageimagesinstagramlinklocation-pinm-swarmSearchmailmessagesminusmoremuplabelShape 3 + Rectangle 1ShapeoutlookpersonJoin Group on CardStartprice-ribbonShapeShapeShapeShapeImported LayersImported LayersImported Layersshieldstartickettrashtriangle-downtriangle-uptwitteruserwarningyahoo

Papers We Love x back-to-back extravaganza

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?

Join or login to comment.

  • Gergo E.

    In follow-up discussion with Soares and Jonas, the topic of representing non-well-typed terms came up, and I mentioned that in the paper, the quotation mapping (which is, remember, not a function written in the language itself) is defined by induction not over terms, but over derivations of well-typed terms.

    To illustrate this, I've tried coming up with a simple example where there's not much detail to conceal the point. The one came up with is turning proofs of well-scopedness for terms of the untyped lambda calculus into a de Bruijn index-based representation:

    So the same way toDB is defined over derivations of well-scopedness, in the paper the quotation mapping is defined over derivations of well-typedness.

    February 9

  • Gergo E.

    Thanks for showing up and the interesting discussions we had after my talk!

    I've uploaded the slides to

    February 6

  • Sergey S.

    Will this meetup be useful for those who can not easily make a typed representation for STLC in Haskell?

    February 1

    • Gergo E.

      The first thing we'll do (after definitions) is coming up with such a representation, so don't worry.

      February 2

People in this
Meetup are also in:

Sign up

Meetup members, Log in

By clicking "Sign up" or "Sign up using Facebook", you confirm that you accept our Terms of Service & Privacy Policy