[TYPES] correctness of closure conversion for untyped lambda calculus wrt. denotational semantics
Neel Krishnaswami
neelakantan.krishnaswami at gmail.com
Tue Oct 2 05:58:15 EDT 2018
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
>
More information about the Types-list
mailing list