[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
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
More information about the Haskell-Cafe
mailing list