[Haskell-cafe] Parsing with Proof

[Wouter Swierstra]

> 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-combinators.pdf

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