Zammit, Vincent (1997) A Proof of the Smn theorem in Coq. Technical report. University of Kent, The University of Kent, Canterbury, Kent, UK (Full text available)
Postscript  
Download (250kB)



Download (276kB)


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<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.
Item Type:  Monograph (Technical report) 

Uncontrolled keywords:  Computability, Theorem Proving, Formalized Mathematics 
Subjects:  Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming, 
Divisions:  Faculties > Science Technology and Medical Studies > School of Computing > Theoretical Computing Group 
Depositing User:  Mark Wheadon 
Date Deposited:  25 Aug 2009 17:26 
Last Modified:  06 Sep 2011 03:57 
Resource URI:  https://kar.kent.ac.uk/id/eprint/21524 (The current URI for this page, for reference purposes) 
 Export to:
 RefWorks
 EPrints3 XML
 CSV
 Depositors only (login required):
Downloads
Downloads per month over past year