[isabelle] Archive of Formal Proofs



Just published at the Archive of Formal Proofs is an entry entitled Recursion Theory I by Michael Nedzelsky. The formalization of more recursion theory would certainly be welcome.

http://afp.sourceforge.net/

Larry Paulson

Entry name:
 Recursion-Theory-I

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).






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.