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

[Jason -Zhong Sheng- Hu]

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

[Ifaz Kabir]

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

[Xuanrui Qi]

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" <***@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

[Jason -Zhong Sheng- Hu]

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-***@inria.fr <coq-club-***@inria.fr> on behalf of Xuanrui Qi <***@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" <***@uwaterloo.ca<mailto:***@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

[sunil]

Post by Jason -Zhong Sheng- Hu
Hi all,
I am wondering if there is already a good practice on turning strings in
Coq into, say, strings in Haskell?

And, this populations increase ,

Post by Jason -Zhong Sheng- Hu
The goal is to push informal part as late as possible, so I am thinking
implementing the to-string functions in Coq as well.

Coq:= a machine, better you understand, better you perform, focus on
understand.

Post by Jason -Zhong Sheng- Hu
This is especially important when the objects are dependent.

Machine can solve this problem.

Post by Jason -Zhong Sheng- Hu
However, these strings need to go to console eventually, so I guess it has
to become string in Haskell some point.

Apropose is a Linux command. Other is grep.

Post by Jason -Zhong Sheng- Hu
My problem is, if this transition is not well-guarded, it sort of defeats
the purpose of pushing informal parts late already.

Human is part of only one fourth of the mother Earth.

Post by Jason -Zhong Sheng- Hu
So how do people normally do this?

Easy, try to understand à€…à€¹à€¿à€‚à€žà€Ÿ.

Post by Jason -Zhong Sheng- Hu
Secondly, is there any framework that can turn a context free grammar into
a certified parser in Coq?

.

Post by Jason -Zhong Sheng- Hu
Thanks,
Jason