coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Improvements to my example arithmetic expression parser

From: David MENTRE <dmentre AT linux-france.org>
To: Daniel Schepler <dschepler AT gmail.com>
Cc: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Improvements to my example arithmetic expression parser
Date: Wed, 5 Sep 2012 09:34:05 +0200

Hello,

2012/8/28 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.

Out of curiosity, how your work is different from the following one?

Jacques-Henri Jourdan, François Pottier, and Xavier Leroy.
Validating LR(1) parsers. In Proceedings of the 21st European
Symposium on Programming (ESOP 2012), volume 7211 of Lecture Notes in
Computer Science, pages 397-416. Springer, March 2012.

http://gallium.inria.fr/~fpottier/publis/jourdan-leroy-pottier-validating-parsers.pdf

Best regards,
david

Re: [Coq-Club] Improvements to my example arithmetic expression parser, David MENTRE, 09/05/2012
- Re: [Coq-Club] Improvements to my example arithmetic expression parser, Daniel Schepler, 09/05/2012
  - Re: [Coq-Club] Improvements to my example arithmetic expression parser, Daniel Schepler, 09/07/2012
    - Re: [Coq-Club] Improvements to my example arithmetic expression parser, Ryan Wisnesky, 09/07/2012