Damien Pous' Home Page.
The class of (μ-)recursive functions forms a rather high-level Turing-complete formalism for partial functions.
Minski machines are a special case of register machines. They are much more operational and low-level than recursive functions, but they have the same expressive power: they are Turing-complete.
During my "DEA" (master) at PPS, I implemented a certified compiler from recursive functions to Minski machines, using the COQ proof assistant. This involved: (1) the formalisation of recursive functions and their semantics, (2) the formalisation of Minski machines, and their operational semantics, (3) the coq-implementation of the compiler itself, and (4), the proof that the compilation process preserves the semantics.
Here are the Coq sources (under GPL), the coqdoc generated gallina; the developments are structured as follows: