A Proof of the S-m-n theorem in Coq.
University of Kent, The University of Kent, Canterbury, Kent, UK
(Full text available)
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<sub>m</sub><sub>n</sub> 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.
- Depositors only (login required):