Tennenbaum's Theorem in its usual form states that for any countable non-standard model $M$ of PA there is no way to code the elements of $M$ as natural numbers such that either the addition or multiplication operation of the model is a computable function on the codes.

Here are two papers by Charles McCarty containing proofs for Tennenbaum's theorem in a constructive setting:

(1) Variations on a thesis: intuitionism and computability (starting on pdf page 26)

(2) Constructive Validity is Nonarithmetic (proof is a bit more detailed)

Working in Heyting arithmetic (HA) instead of PA he further assumes that the models behave constructively as well. Below, I will list the main steps of the proof as I see them. For any HA Model $M$, I will call $a \in M$ standard an write $\operatorname{std}(a)$ iff there is an $n \in \mathbb{N}$ with $\overline{n} = a$, where $\overline{(\cdot)} : \mathbb{N} \rightarrow M$ is the canonical embedding.

• Let $a \in M$ with $\neg \operatorname{std} a$. One can show that it is greater than any numeral $\overline{n}$.
• There are recusively inseperable sets $A, B$ represented by $\Sigma_1$ formulas $\alpha(x), \beta(x)$.
• For any unary predicate $\varphi$ you can show $HA \vdash \forall x ~\neg \neg \forall y < x ~ \,( \varphi(y) \, \lor \, \neg \varphi(y)\,)$
• Using soundness and instantiating the above for $\alpha$ and $a$ we get $M \vDash \neg \neg \forall y < a. ~\,( \alpha(y) \, \lor \, \neg \alpha(y)\,)$
• We are trying to prove $\bot$, so we can get rid of the $\neg \neg$ in the above and since any numeral $\overline{n}$ is smaller than $a$ we get $(M \vDash \alpha(\overline{n}) ) \lor (M \vDash \neg \alpha(\overline{n}))$.
• Models are considered to be constructive, so the above $\lor$ means we have a decider which we can use to define a function by $f(n) = 0 ~\Leftrightarrow~ M \vDash \alpha(\overline{n})$.
• By Church's Thesis, the function $f : \mathbb{N} \rightarrow \mathbb{N}$ is recursive and seperates $A$ and $B$, leading to a contradiction.

So far this shows $\neg \exists a \in M ~ \neg \operatorname{std}(a) ~\Leftrightarrow~ \forall a \in M ~ \neg \neg \operatorname{std}(a)$.

Further assuming Markov's Principle, we immediately get $\forall a \in M ~\, \operatorname{std}(a)$, showing that Heyting arithmetic is categorial.

I have done a mechanized proof of Tennenbaum in Coq, based on the presentations in articles of Peter Smith and Richard Kaye. The articles by McCarty were only a recent find by my advisor. They were not referenced by Smith or Kaye and there don't seem to be a lot of publications out there citing them, so I would be happy about anyone who can comment on them, maybe putting it into a larger context.