Lambda the Ultimate

Hi all,

I'm looking for literature which focuses on proving context-free parsers correct. For example, I have work by Sikkel on Parsing Schemata and work by Cliff Jones on formalizing Earley's algorithm, and looking for other ways that people have formalized and proved those (and other context-free) parsers.

Thanks for any recommendations,
Dan