The Coq mailing list

[Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>]

Hi Xuanrui, Ifaz,

I took a quick look at Menhir's refman. Actually it has a coq backend. Ultimately it's coq that does the verification, so I think it's fine. It has caught a few of my typos. Compcert seems to also do it in this way. However, what's certified in Menhir's output is that the parser is sound wrt to the grammar. It's one step closer to string -> ast, but lexer is missing now.

Sincerely Yours,

Jason Hu

---

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Xuanrui Qi <xqi01 AT cs.tufts.edu>
Sent: October 5, 2018 1:28 PM
To: Coq Club
Subject: Re: [Coq-Club] Connecting strings in Coq and extraction target?

 

Jason and Ifaz:

I'm not sure Menhir generates a verified parser, though. If I recall correctly, verified parsing is still a quite active research topic.

-Xuanrui

On Fri, Oct 5, 2018 at 12:06 PM -0400, "Ifaz Kabir" <ikabir AT uwaterloo.ca> wrote:

Hi Jason,

I can't comment on the strings part, but Menhir (an OCaml parser generator) can produce Coq parsers.

-Ifaz

From: Jason -Zhong Sheng- Hu

Sent: Friday, October 5, 9:56 AM

Subject: [Coq-Club] Connecting strings in Coq and extraction target?

To: Coq Club

Hi all,

I am wondering if there is already a good practice on turning strings in Coq into, say, strings in Haskell? The goal is to push informal part as late as possible, so I am thinking implementing the to-string functions in Coq as well. This is especially important when the objects are dependent. However, these strings need to go to console eventually, so I guess it has to become string in Haskell some point. My problem is, if this transition is not well-guarded, it sort of defeats the purpose of pushing informal parts late already. So how do people normally do this?

Secondly, is there any framework that can turn a context free grammar into a certified parser in Coq?

Thanks,

Jason