Proof-Producing Synthesis of CakeML from Coq

Coq's extraction plugin is used to produce code of a general purpose

  programming language from a specification written in the Calculus of Inductive

  Constructions (CIC). Currently, this mechanism is trusted, since there is no

  formal connection between the synthesized code and the CIC terms it originated

  from. This comes from a lack of formal specifications for the target

  languages: OCaml, Haskell, and Scheme. We intend to use the formally specified

  CakeML language as an extraction target, and generate a theorem in Coq that

  relates the generated CakeML abstract syntax to the CIC terms it is generated

  from. This work expands on the techniques used in the HOL4 translator from

  Higher Order Logic to CakeML. The HOL4 translator also allows for the

  generation of stateful code from the state and exception monad. We expand on

  their techniques by extracting terms with dependent types, and generating

  stateful code for other kinds of monads, like the reader monad, depending on

  what kind of computation the monad intends to represent.