The Coq mailing list

[Xuanrui Qi <xqi01 AT cs.tufts.edu>]

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