Damien Pous' Home Page.

A certified compiler from recursive functions to Minski machines

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:

Notice that Coq 8.0 is required in order to succesfully check those developments: in latter versions, there was some a changes in tactics behaviour, so that I have to fix my own tactics.