[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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.s...@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 > > > >