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 definition of a computable function, proofs of the computability of a number of functions and the definition of an effective 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.