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:

• 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.