coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Recursive Notations and LL1 parsing

From: Qiang Liu <lqiangecnu AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Recursive Notations and LL1 parsing
Date: Wed, 17 Mar 2010 13:29:25 +0800
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :content-type; b=s+Iym3Ph9aWlqrPS9jzJJbDFFnyHoRWhIR+NBXPOwu84Rg1bMm7YcBXP4M98/v65Qq 2fmfaFL0tIDhDuenzf+HLUlvS4/Ag9uMeuCbJNgrXvu5lr+Ok63jjLPnk0ykPo30Ouqe ZvIX4YI6cgmt978ikzRSBVutD23FgjYqEapz4=

hi, everyone. I seems to need to develop a verified software in the Coq system. I recently heard the Coq related tool YNot, �a imperative extention of Coq? can it actually allow infinite loop?(un-termination), if it does, can anyone explain how it does this? Can programs written in YNot still be verified by the Coq proof system ? �thanks a lot!�

[Coq-Club] Recursive Notations and LL1 parsing, Christian Doczkal
- Re: [Coq-Club] Recursive Notations and LL1 parsing, Hugo Herbelin
  - Re: [Coq-Club] Recursive Notations and LL1 parsing, Qiang Liu
    - Re: [Coq-Club] Recursive Notations and LL1 parsing, Adam Koprowski