[POPLmark] A compilation challenge problem

[Adam Chlipala]

I've written up a POPLmark-style benchmark problem distilled from a real 
problem that came up in the course of a project I'm working on:
    http://www.cs.berkeley.edu/~adamc/poplmark/compile/

In essence, this problem is about proving the correctness of a compiler 
from a high-level lambda calculus to a lower-level imperative language, 
where aggregate data must be represented in an untyped heap, with manual 
memory management.

I've also posted my solution to this challenge, which brings together 
some ideas I've been playing with involving formalizing language 
metatheory in Coq using Debruijn indices and denotational semantics.  
I'd be really curious to read any feedback on this (unconventional) 
approach, and especially to see any implementations using one or both of 
HOAS and operational semantics that lead to more manageable code bases.