coq-club AT inria.fr

Subject: The Coq mailing list

List archive

chronological Thread

From: Ashish Darbari <ashish_darbariuk AT yahoo.co.uk>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] Arrays in Coq
Date: Fri, 2 Jan 2009 13:15:59 +0000 (GMT)
Domainkey-signature: a=rsa-sha1; q=dns; c=nofws; s=s1024; d=yahoo.co.uk; h=X-YMail-OSG:Received:X-Mailer:Date:From:Reply-To:Subject:To:MIME-Version:Content-Type:Message-ID; b=FrCld7dFvEjDlkWk/gDWYUYNF5wUK1oq5/EQVG9bJtUrfpLXpUKVDZCmqsntDzy/RFuxsxls+708otkZbQkzgZm8AEUi7s13Rcv10bBeynos9xds5Md1PYPeKLLyYmi4AuJhFUBE7pp/PHgVdlkRsyM61luGuPsVDGcfOuJfup8=;
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Is there an implementation of Arrays in Coq? If yes, does someone have any experience on

extraction to ocaml arrays?

I can't seem to find much on it, except for some work done by Jean-Christophe Filliatre

perhaps as a part of QuickSort implementation, but in the quicksort tar ball there is no

array module, and though I found an array implementation (see attachment) elsewhere on the web (by Filliatre)

- this implementation is axiomatized and it relies on ProgInt module that

my Coq 8.1.pl4 can't find.

Any help is greatly appreciated.

Thanks

Ashish

Attachment: Arrays.v
Description: Binary data

[Coq-Club] Arrays in Coq, Ashish Darbari
- Re: [Coq-Club] Arrays in Coq, Adam Chlipala