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

Jeremy Siek <[email protected]>
Newsgroups gmane.comp.science.types
Message-ID <[email protected]> 
[ 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
lmpx.com only provides a reader for public news (NNTP) servers. It is not affiliated with the servers or forums shown here and is not responsible for the content of articles, which is written by their respective authors.