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


Larry Paulson

Entry name:

 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.