© University of Kent - Contact | Feedback | Legal | FOI | Cookies
A proof of the S-m-n theorem in Coq
Vincent Zammit
Technical Report 9-97, The Computing Laboratory, The University of Kent, Canterbury, Kent, UK, March 1997.Abstract
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.
Download publication 244 kbytes (PostScript)
Bibtex Record
@techreport{227, author = {Vincent Zammit}, title = {A Proof of the {S}-m-n theorem in {C}oq}, month = {March}, year = {1997}, pages = {182-196}, keywords = {determinacy analysis, Craig interpolants}, note = {}, doi = {}, url = {http://www.cs.kent.ac.uk/pubs/1997/227}, address = {The University of Kent, Canterbury, Kent, UK}, institution = {The Computing Laboratory}, number = {9-97}, }