School of Computing

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},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014