coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Ana Borges <ana.agvb AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Reading text from a json / xml file
Date: Tue, 11 Sep 2018 12:11:28 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=ana.agvb AT gmail.com; spf=Pass smtp.mailfrom=ana.agvb AT gmail.com; spf=None smtp.helo=postmaster AT mail-pf1-f171.google.com
Ironport-phdr: 9a23:6xfDXRPN1dVUnHnEAfsl6mtUPXoX/o7sNwtQ0KIMzox0LPvyrarrMEGX3/hxlliBBdydt6obzbKO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxlKiTanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0yRD+s7bpkSAXwhSgINzA3/mLZhNFugq1Hux+uvQBzzpTObY2JKPZzfKXQds4aS2pbWcZRUjRMD5+6b4QVEuEMIOFYr5Pyp1QQthu1GA6hC/npyjBSnHP5x6I60/o6Hgzd0wwgGsgBsHXQrNnvKKgSVuW1wbDOwD7ebP1WwS/w5JbUfh0lu/2BXrJ9fdDPxUUyCw/JlEicpI74Mz6Ty+8DqXKU7/B6WuKqk2Mnqx9+ojyoxso0j4nGnIMVylTd+SVhzoY5OMS0SEBmbdOmDZdcrS6aN4xxQsMtR2Fnpjw2xaEBuZ6+ZCQKyZInyADDa/GfbYSE/hbuWPySLDp4nn5pZq+ziwqo/US9yODwS9G40FNQoSpEltnMuGoN1xvW6sWfUPR9+F2u1SyV2ADc9OFLOls5laXeK5E7w74wkoAfvljEHi/zgEn2lrOZdl04+ui07OTqeqnpppiFN4Ntlg7+NrkuldekDOQjMgkOWnCb9v6m2L3i+035WrRKgecsnqnXqpCJbfgc86W+Gkpe1pspwxe5FTavltoCzlcdK1cQURSOx6LuIV7DO7isBPG2xV2jjj1DyPXPP7mnCZLIeCuQ2Iz9dKpwvhYPgDE4yspSssoNW+MxZcnrU0q0j+T2SxowMgi62eHiUYwv2YYXWGbJCaicYvqL7Q24o9k3KuzJX7c7/S7nIqF8tfHrhH4931QaePvxhMZFWDWDBv1jZn6hTz/sj9MGSzlYuwM/SKnyhgTHX2cMPjC9WKUz4jx9A4WjX9/O

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