  Formally reasoning about functional programs is supposed to be
straightforward and elegant, however, it is not typically done as a matter of
course. Reasoning in a proof assistant requires "reimplementing" the code in
those tools, which is far from trivial. SMLtoCoq provides an automatic
translation of SML programs and function contracts into Coq. Programs are
translated into Coq specifications, and function contracts into theorems, which
can then be formally proved. Using the Equations plugin and other well
established Coq libraries, SMLtoCoq is able to translate SML programs without
side-effects containing partial functions, structures, functors, records, among
others. Additionally, we provide a Coq version of many parts of SML's basis
library, so that calls to these libraries are kept almost as is.
