Nested datatypes with generalized Mendler iteration: map fusion and the example of the representation of untyped lambda calculus with explicit flattening

All the following code is additional material to the article of the same name by the author that was presented at MPC 2008 (proceedings appeared in LNCS).

THIS IS THE OLD MPC2008 CODE, THE ONE FOR THE JOURNAL SCP IS ONE DIRECTORY HIGHER!

the ZIP file with the Coq scripts
lame.hs (NEW: example with Haskell)
LNGMItPred.v
LNGMItImp.v
LamPred.v
EFlatPred.v
LNMItPred.v
LNMItImp.v

The latter two come from the extra material for the JFP paper this work is based on (my publications page).

Ralph Matthes