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:

`vector.v`

:- type of lists whose length is specified (vectors),
- miscellaneous utilities about these vectors.

`recursive.v`

:- formalisation of recursive functions,
- correctness of their semantics,
- some examples.

`minski.v`

:- formalisation of Minski machines,
- correctness of their semantics.

`minski_tools.v`

:- tools for manipulating Minski machines: shifting, concatenation, loops...

`minski_ops.v`

:- standard operations using Minski machines: copy, move...

`compilation.v`

:- actual compilation function,
- proof of correctness of that function.

`examples.v`

:- some examples.