coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] Connecting strings in Coq and extraction target?
Date: Fri, 5 Oct 2018 15:55:35 +0000
Accept-language: en-CA, en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=fdhzs2010 AT hotmail.com; spf=Pass smtp.mailfrom=fdhzs2010 AT hotmail.com; spf=Pass smtp.helo=postmaster AT NAM03-BY2-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:Hws7fxbNEWGsqLJJd6ISiy//LSx+4OfEezUN459isYplN5qZr8u4bnLW6fgltlLVR4KTs6sC17KJ9fi4EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCa/bL9oMBm6sRjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjm58axlVAHnhzsGNz4h8WHYlMpwjL5AoBm8oxBz2pPYbJ2JOPZ7eK7WYNEUSndbXstJVyJPHJ6yb5cBAeQCIelXoJLwqEESoReiHwSgGP/jxiJOi3Tr3aM6yeMhEQTe0QIkBd0Oq3PUrNPoP6sLUu+1zK7IzTPMb/hLxDn96JbHchYuof2VQLl+c9fRwlQoGgPLk1qQqY3kPyiL2ugRrmSX8/FtVeKoi247rgF+uDmvxsM2hobVgYIVz0nJ+CNky4g2Pd21UFB3bcOlHZdKuSyWKZF6Tt4hTm10oio3yrwLtYa1fCcUy5kr2xvSZvmdfIWM/B7sT+OcLSp6iX1+drKyghW//la7xeD5V8S7y1hKoTFDn9LRrH4CzQbT5dKCSvZl/keuxzKP1wfL5+9cPU06krbXJpA4zrMtlJUfr13PHijtl0rolqOWcVgk+vSz5OTgf7XmoIKTO5VsigHkNaQuhtKwDvgkMggPWGib//6w1Lr+/U3lRLVKifo2kqrDvJ/GIsQbo7a1Aw5T0ok99xayFymq3MkZkHUdIl9JZgiLg5XqNl3SOvz1Dfayj0ypkDhxxvDGOrPhAo/KLnjGiLrhc6ty605dyQoo09xT+49YBq0aLfLzXU/xqNnYAQU4Mwyw2eroFNJ91oYGVWKVHqCZKL/SsUOP5u83P+aMY5YVtC/hJPgh+v7hlmQ0mUQdfKmsxZsYcmq0HvVgI0WDYHrjmM0NEWkQvll2cOu/o1qbGRVXenz6C6k7/3QwDJ+sJYbFXIGkxrKbinSVBJpTM0JPEVeKWTLad4KCVL83aC+ULYopsiFMAbatS506j0n37Cf6zKZiJ+vQvCYfsMSwh5BO++TPmERqpnRPBMOH3jTIFjksxzJad3oNxKl65HdF5BKG2Kl8jeZfEIUItfNOTgIzNJqaxOt/WYmrBlDxO+yRQVPjee2IRCkrR4tqkd8Jf0N0GtHkhRfGjXLzXu0l0oeTDZlxyZrymnj8I8EhlCTg/Yx51BwMc5EKMmerwKli6wLUGojF1V2DkLqnfrgd2yiL83qfyW2JvwdTVwsiCKg=

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

[Coq-Club] Connecting strings in Coq and extraction target?, Jason -Zhong Sheng- Hu, 10/05/2018
- Re: [Coq-Club] Connecting strings in Coq and extraction target?, Ifaz Kabir, 10/05/2018
  - Re: [Coq-Club] Connecting strings in Coq and extraction target?, Xuanrui Qi, 10/05/2018
    - Re: [Coq-Club] Connecting strings in Coq and extraction target?, Jason -Zhong Sheng- Hu, 10/05/2018
- Re: [Coq-Club] Connecting strings in Coq and extraction target?, sunil, 10/05/2018