The Coq mailing list

[Helmut Brandl <helmut.luis.brandl AT gmail.com>]

Hello all,

I am writing a verifying compiler and I use ocaml as the implementation
language. I would like to use coq to verify some critical algorithms.

I have already read some documentation on program extraction. With
inductive types I don't see any problems, because inductive types and
functions on inductive types are translated one to one (with some
lexical adaptions and proof deletion) from coq to ocaml.

However I need arrays and I need to index arrays with ints in my
program. The algorithms I am trying to verify do not use the mutability
of ocaml arrays but they use the contents.

Can anybody give me hints (or links to any documentation) on how to
represent arrays and ints in coq?

Thanks
Helmut