Recursion-Theory-I

 

Title:	Recursion Theory I
Author:	Michael Nedzelsky
Submission date:	2008-04-05
Abstract:	This document presents the formalization of introductory material from  recursion theory --- definitions and basic properties of primitive recursive  functions, Cantor pairing function and computably enumerable sets  (including a proof of existence of a one-complete computably enumerable set  and a proof of the Rice's theorem).

 

Proof outline Proof document

Browse theories

Download this entry

Older releases: Isabelle 2009: afp-Recursion-Theory-I-2009-04-29.tar.gz Isabelle 2008: afp-Recursion-Theory-I-2008-06-10.tar.gz Isabelle 2007: afp-Recursion-Theory-I-2008-04-11.tar.gz