Have you seen Arthur Charguéraud's PhD thesis, Characteristic Formulae for Mechanized Program Verification?
Rather than building the type system and small-step semantics as inductive relations, he gives a technique for converting Caml programs into characteristic formulas. This are basically a generalization of predicate transformer semantics to support a very large subset of Ocaml -- notably, including unsafe casts like
Obj.magic. To quote from his thesis:
I have focused on a subset of the OCaml programming lan-
guage, which is a sequential, call-by-value, high-level programming language. The
current implementation of CFML supports the core λ-calculus, including higher-
order functions, recursion, mutual recursion and polymorphic recursion. It supports
tuples, data constructors, pattern matching, reference cells, records and arrays. I
provide an additional Caml library that adds support for null pointers and strong
It's a very appealing approach if you want to prove a particular Caml program correct (less so if you are interested in its metatheory, though).