The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

One of the questions you asked was about having libraries that help 
using extracted code.

One point of view is to have a "run-time" environment for extracted 
code, that provides basic input-output facilities for extracted code.  I 
started developing one such environment.  There is a very preliminary 
description of what I have in mind on the following page:

http://www.lix.polytechnique.fr/cocorico/ZInterfacePackage

I have since added string support.

I don't think this corresponds to what you have in mind, since you 
insist more on large scale developments,
binding with existing ocaml or haskell code, etc.  But maybe this can be 
useful.

Yves