The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

I've just spent some time writing a certified parser, as I couldn't
find any examples in Coq of such a thing with a quick Google search,
and I was curious how the proofs might look.  (I did see a parser for
something called IMP, I think; but it wasn't certified as to
correctness or completeness with respect to any formal grammar, and
furthermore it didn't bother to prove termination, just passed in a
bound on recursion depth.)  It's not very short (but also not
extremely long), so I posted it at
http://coq.inria.fr/cocorico/ArithmeticExpressionParser .  There are
still a couple points that I'd like to improve, but I can't quite
figure out how:

The major one is that in the proof of completeness of the parser, I
pretty much had to do everything by hand for each rule of the grammar.
 I've been trying to figure out how I could automate the proof more,
without much success.

It would also be nice if I could write the body of parse_expr_sub, for
example, as

(
do t <- peek_token;
match t with
| Some PLUS =>
  get_token >>
  do m <- parse_summand;
  parse_expr_sub (n + m)
| Some MINUS =>
  get_token >>
  do m <- parse_summand;
  parse_expr_sub (n - m)
| _ => return_ n
end
) l H

and so on; but still have the Program system generate the appropriate
obligations used for proving termination.  I can't quite seem to find
proper definitions of the notation that will allow that.
-- 
Daniel Schepler