I am wondering about how to give a correctness prove of a simple parsing algorithm. I tried to think of a simple example but even in this case I don't know how.
I'm not sure I understand your question, but I'm guessing you're looking for general techniques for the formal verification of combinator-based parsers. Here's a quick brain dump of related work that might help you get started. Nils Anders Danielsson wrote a verified regexp matcher in Agda a while ago. http://www.cs.chalmers.se/~ulfn/darcs/Agda2/examples/AIM6/RegExp/ Although this isn't quite parsing, the ideas are relatively simple so it's a good place to start. (Bob Harper has a theoretical pearl on the topic, which might be worth checking out to get some inspiration). More recently, Nils Anders has extended this to parser combinators together with Ulf Norell: http://www.cs.nott.ac.uk/~nad/publications/danielsson-norell-parser-combinat... Alternatively, you could explore how to implement similar ideas in Coq. I'm a big Program fan and recently used it to verify some simple programs in the state monad. I've just submitted a paper about this: http://www.cse.chalmers.se/~wouter/Publications/HoareStateMonad.pdf I'd imagine you might be able to take a similar approach to applicative (or monadic) parser combinators. Doaitse Swierstra recently wrote a good overview tutorial about parser combinators in general that is certainly worth checking out: http://www.cs.uu.nl/research/techreps/repo/CS-2008/2008-044.pdf Hope this helps, Wouter