The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Ashish Darbari wrote:
> Is there an implementation of Arrays in Coq? If yes, does someone have 
> any experience on 
> extraction to ocaml arrays?

Since Coq's Gallina is a purely functional language, a direct 
implementation of the (imperative) array ADT doesn't make sense.  
Nonetheless, arrays tend to be easy to integrate into approaches to 
describing and verifying imperative programs in Coq.  For instance, 
arrays are included in the latest version of the Ynot system, which we 
hope to release in the next few weeks.