[TYPES] correctness of closure conversion for untyped lambda calculus wrt. denotational semantics

[Gabriel Scherer]

Dear Jeremy,

In what sense would closure conversion be correct for the untyped
lambda-calculus? Writing in an untyped language allows me to use pair/tuple
operations to access the closure environment, which was not previously
possible on the non-closure-converted calculus. If your untyped target
language (I think it should be made precise) contains a primitive
representation of closures (not just pairs), you can prevent environment
extraction, but then that corresponds to your third bullet of a target that
"supports (explicit) closure creation".

Best

On Mon, Oct 1, 2018 at 11:11 PM Jeremy Siek <jeremy.siek at gmail.com> wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list
> ]
>
> I’m interested in finding literature on proofs of correctness of closure
> conversion
> applied to the untyped lambda calculus with respect to a denotational
> semantics.
> (Bonus for mechanized proofs.)
>
> I’ve found papers that are a near miss for what I’m looking for, such as:
> * closure conversion proofs for the STLC (Chlipala PLDI 2007)
> * closure conversion proofs based on operational semantics
>    (Minamide, Morrisett, and Harper POPL 1996, and many more)
> * correctness proofs using denotational semantics for compilers that
>    don’t do closure conversion, but instead compile to a machine that
>    supports closure creation (the VLISP project and many more).
>
> Thanks in advance for pointers!
>
> Best regards,
> Jeremy
>
>