This thesis presents a formal development of basic computability theory in constructive type theory. The entire development is carried out in the proof assistant Coq. No classical assumptions are needed for the development.
We base our theory on a minimal functional programming language obtained as a variant of the weak call-by-value lambda calculus. The choice of the programming language is crucial since in a formal development of computability theory complex constructions must be programmed and verified that are merely sketched in standard textbooks.
We show basic undecidability results including the theorems of Scott and Rice. This is the easy part of the formal development. The construction and verification of a step-indexed self-interpreter (universal program) and a dovetailing self-interpreter is considerably more involved. We show that a logically decidable problem is computationally decidable if it is acceptable and co-acceptable. We also show that a problem is acceptable if and only if it is enumerable. Finally, we prove that termination for all arguments is neither acceptable nor co-acceptable.