[Coq-Club] Reading text from a json / xml file

[Ana Borges]

Dear Coq useres,

My goal is to use Coq to extract formalized code in OCaml. This code would
start by parsing a json file (or xml), then it would do some computations,
and finally it would output a json / xml file.

Ideally, I would like to have every part of the process formalized. In
particular, I would like to have proof that the parsing process didn't
introduce any bugs.

I tried searching for existing Coq libraries to do something of this sort,
but didn't find any. I know there are OCaml libraries, and in the worst
case I would formalize only the "middle" part of the program in Coq, and
write the rest directly in OCaml.

Do you know if this or something similar has been done before? Do you have
an idea of how hard / time consuming it would be?

Thank you very much,
Ana Borges

[Théo Zimmermann]

Hi,

Menhir has some support for formally verified parsers, see
http://gallium.inria.fr/%7Efpottier/menhir/manual.html#sec75.
I've never used this so I can't say much more but I'm pretty sure that
there are users on this list who can answer any further questions you may
have.

Cheers,
Théo

Post by Ana Borges
Dear Coq useres,
My goal is to use Coq to extract formalized code in OCaml. This code would
start by parsing a json file (or xml), then it would do some computations,
and finally it would output a json / xml file.
Ideally, I would like to have every part of the process formalized. In
particular, I would like to have proof that the parsing process didn't
introduce any bugs.
I tried searching for existing Coq libraries to do something of this sort,
but didn't find any. I know there are OCaml libraries, and in the worst
case I would formalize only the "middle" part of the program in Coq, and
write the rest directly in OCaml.
Do you know if this or something similar has been done before? Do you have
an idea of how hard / time consuming it would be?
Thank you very much,
Ana Borges