Traditional recursion theory is the study of computable functions on the natural numbers. This thesis considers recursion theory in first-order arithmetical theories and categories, thus expanding the work of Ritchie and Young, Lambek, Scott, and Hofstra. We give a complete characterisation of the representability of computable functions in arithmetical theories, paying attention to the differences between intuitionistic and classical theories and between theories with and without induction. When considering recursion theory from a category-theoretic perspective, we examine syntactic categories of arithmetical theories. In this setting, we construct a strong parameterised natural numbers object and give necessary and sufficient conditions to construct a Turing category associated to an intuitionistic arithmetical theory with induction.

The concept of a recursive function has been extensively studied using traditional tools of computability theory. However, with the development of category-theoretic methods it has become possible to study recursion in a more general (abstract) sense. The particular model this thesis is structured around is known as a Turing category. The structure within a Turing category models the notion of partiality as well as recursive computation, and equips us with the tools of category theory to study these concepts. The goal of this work is to build a formal language description of this computation model. Specifically, to use the Coq proof assistant to formulate informal definitions, propositions and proofs pertaining to Turing categories in the underlying formal language of Coq, the Calculus of Co-inductive Constructions (CIC). Furthermore, we have instantiated the more general Turing category formalism with a CIC description of the category which models the language of partial recursive functions exactly.