[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Hi Jeremy, One approach to closure conversion which I like very much is the observation that when you defunctionalize a normalization- by-evaluation algorithm, you get a translation into an explicit closure representation. I learned this from Chapter 3 of Andreas Abel's habilitation thesis [1], where he abstracts NbE from domains to partial applicative structures, and then shows that a closure calculus forms a partial applicative structure. This might be too operational for you, but since the line between operational and denotational approaches can get pretty blurry, perhaps it is of interest. [1] <http://www.cse.chalmers.se/~abela/habil.pdf> Best, Neel On 01/10/18 20:14, Jeremy Siek 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
