A proof of the S m n theorem in Coq

This report describes the implementation of a mechanisation of the theory of computation in the Coq proof assistant which leads to a proof of the S m n theorem. This mechanisation is based on a model of computation similar to the partial recursive function model and includes the denition of a computable function, proofs of the computability of a number of functions and the denition of an eective coding from the set of partial recursive functions to natural numbers. This work forms part of a comparative study of the HOL and Coq proof assistants