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



Download (276kB)
Preview


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 > Sciences > School of Computing > Theoretical Computing Group 
Depositing User:  Mark Wheadon 
Date Deposited:  25 Aug 2009 17:26 UTC 
Last Modified:  28 May 2019 14:00 UTC 
Resource URI:  https://kar.kent.ac.uk/id/eprint/21524 (The current URI for this page, for reference purposes) 
 Export to:
 RefWorks
 EPrints3 XML
 BibTeX
 CSV
 Depositors only (login required):