As often in these matters, the encodings are important: you could have some silly encoding of Turing machines or Gallina terms or both where an input string $\langle n\rangle$ represents "the $n$-th well-typed term in Gallina". The TM that accepts this is trivial, and you'd be able to prove correctness and termination of the machine easily.
See e.g. this Mathoverflow question: https://mathoverflow.net/questions/223109/does-the-notion-of-provably-total-function-depend-on-the-chosen-representation
However, for any reasonable representation, any proof that the "usual" type checking algorithm terminates implies termination of reduction for well-typed terms, which in turn implies consistency of the underlying logic as suggested here. This is impossible if Coq/Gallina is actually consistent, per the second incompleteness theorem.
Two obvious fixes:
Add consistency of Coq (or some equivalent or stronger statement) to your list of axioms. One possible axiom is: consistency of ZFC + $\omega$-many inaccessible cardinals. If you want something more computational, you can add a strong enough form of induction-recursion. I don't think anyone's worked out the details for the CiC yet, but I imagine they're very similar to those for (for instance) Agda.
Add some constraints on the representation of well-typed terms to be checked. In Gallina, terms carry implicit computational content, to be executed as the usual type-checking algorithm runs. However one could imagine an explicit form of the language, where each term comes with a natural number representing the "gas" it is allowed to use, aka the number of steps it must not exceed during reduction. Then the correctness proof for the type-checking algorithm would be conditional on not exceeding this explicit limit of computation.
Note that talking about computability of these axioms doesn't make much sense: a single axiom on it's own is always computable in the sense of computable sets which is usually what we mean when we talk about computable theories.
However an axiom may or may not have computational content, for example an axiom $\exists x,\ P$ may cause a theory to lose the existence property, if there is no closed term $t$ which satisfies $P[t/x]$. However, an axiom that asserts that a Turing machine $T$ halts on all inputs is always correct from a computable (constructive) point of view if $T$ does indeed always halt in the "true" world.