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

[Jeremy Siek]

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