Proof-Producing Translation from Gallina to CakeML

Users of theorem provers often desire to to extract their verified code to a  more efficient, compiled language. Coq's current extraction mechanism provides this facility but does not provide a formal guarantee that the extracted code has the same semantics as the logic it is extracted from. Providing such a guarantee requires a formal semantics for the target code. The CakeML project, plemented in HOL4, provides a formally defined syntax and semantics for a subset of SML and includes a proof-producing translator from higher-order logic to CakeML. We use the CakeML definition to develop certifying extractor to CakeML from Gallina using the translation and proof techniques of the HOL4 CakeML translator. We also address how differences between HOL4 (higher-order logic) and Coq calculus of constructions) effect the implementation details of the Coq translator.