coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Théo Zimmermann <theo.zimmi AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Reading text from a json / xml file
Date: Wed, 12 Sep 2018 13:59:43 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=theo.zimmi AT gmail.com; spf=Pass smtp.mailfrom=theo.zimmi AT gmail.com; spf=None smtp.helo=postmaster AT mail-ua1-f46.google.com
Ironport-phdr: 9a23:dUegaBbhROB3eS7Cbu1tNmf/LSx+4OfEezUN459isYplN5qZoM+8bnLW6fgltlLVR4KTs6sC17KJ9fi4EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCa/bL9oMBm6sRjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjmk8qxlSgLniD0fOjE2/mHYiMx+gqxYrhy8uRJw35XZb5uJOPdkZK7RYc8WSGhHU81MVyJBGIS8b44XAuQfPeZftY79qEMNohu/AAmsAf3gyiVNhnDs26061fkqHAba3AwgAd0Ot27YrdT0NKcXVOC1zbLFzTrGb/xM2Df97JLEfQwmofGJRL99d9fax0coFwPAlFqQqIrlMiuU1uQLqWib7vBvWfihi249rQx6vzuhxt80h4XXmo4YzkrI+CZ5zYovO9G0VlB3bcSrHZZRsSyRKpF4Tdk4Q25yvSY30r0GtoC/fCgN0JknwgTQa/2Dc4SR/xLsTvudLS52hH9qeb+znRmy8U+nyu3zUsm7zkxGoTZCktnJrnwN1hrT5dabSvZl4EutxTKC2xrQ5+xEO0w4i7TXJ4A7zrM/l5cfqUHDETX3mEXygq+WbEIk+u2w5uT7YrXpuJicO5V1iwH/N6Qun82/DP83MggLRWeb+OC82Kf/8k3+RbVGluc2nbXBsJDGOcQboba0DBNS0oY68hqwEzOm0MkDknQcN1JEeBeHj5DzNF3UIfD4C+2/g1W2nztxyfDGJO6pPpKYJX/a1bzlYLxV6khGyQN1w8oMyYhTD+Q9IHP0bX3wsdnVFBowNQr8l/rnBdI7xIIbXGOnDaqQMaeUuliNsLF8a9KQbZMY7W6uY8Mu4OTj2CdgyA0tOJKx1J5SU0iWW/FvIkGXe33p245THmIDvw54R+vv2gTbDWxjIk2qVqd53QkVTZq8BN6aFI+oib2Fmiy8G88OPz0UOhW3CX7tMr68dbIMZSaVeJIzlzUFUf28QtZk203w8gD9zLVjI6zf/ShK7Z8=

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

Le mar. 11 sept. 2018 à 12:12, Ana Borges <ana.agvb AT gmail.com> a écrit :

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

[Coq-Club] Reading text from a json / xml file, Ana Borges, 09/11/2018
- Re: [Coq-Club] Reading text from a json / xml file, Théo Zimmermann, 09/12/2018