[TYPES] correctness of closure conversion for untyped lambda calculus wrt. denotational semantics
jeremy.siek at gmail.com
Mon Oct 1 15:14:16 EDT 2018
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!
More information about the Types-list