The Coq mailing list

[Kevin Sullivan <sullivan.kevinj AT gmail.com>]

With apologies in advance for not being adequately aware of the science in this dimension, the question I ask is whether Coq extraction has been viewed or formalized as a functor, e.g., from a category of Coq Specs to a category of Haskell or OCaml programs? I ask because I'm interested in synthesizing other kinds of things from Coq specs (in possibly partially forgetful ways) and I haven't found the appropriate literature on the science underlying extraction.

Kevin