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

[Jeremy Siek]

Hi Gabriel, William,

Yes indeed, it was just whole program correctness that I had in mind, and not fully abstract compilation.

-Jeremy

> On Oct 1, 2018, at 5:28 PM, William J. Bowman <wjb at williamjbowman.com> wrote:
> 
> 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
>>> 
>>>