The Coq mailing list

[Adam Koprowski <adam.koprowski AT gmail.com>]

On Wed, Mar 17, 2010 at 06:29, Qiang Liu <lqiangecnu AT gmail.com> wrote:

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! 

  Dear Quianq,

  please do not reply to a random thread while posting questions (your question has nothing to do with parsing, right?).

  As for Ynot, to the best of my knowledge: 

• yes, you can write non-terminating programs and have imperative computations and pointers with Ynot,
• to achieve that Ynot axiomatizes a parametrized monad (see ST.v in the distribution of Ynot) and during extraction those axioms are replaced with imperative computations in Ocaml (see STimpl.ml in the distribution of Ynot)
• sure, you can verify Ynot programs with Coq, that's the whole point of this library

  Best,

  Adam

--
Adam Koprowski   [http://www.cs.ru.nl/~Adam.Koprowski]
R&D @ MLstate    [http://mlstate.com, 15 rue Berlier, 75013 Paris, France]