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

[William J. Bowman]

Gabriel,

It sounds like you're describing a failure of full abstraction.
I think the compiler could still satsify "whole-program correctness", i.e., the
translated (whole) program denotes the same value as the original, even without
primitive closures.

--
William J. Bowman

On Mon, Oct 01, 2018 at 11:26:31PM +0200, Gabriel Scherer wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 
> 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
> >
> >