[Haskell-cafe] Parsing with Proof

Wouter Swierstra wss at cs.nott.ac.uk
Wed Apr 1 06:12:22 EDT 2009

> 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  


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:


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:


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:


Hope this helps,


More information about the Haskell-Cafe mailing list