Gentzen's Hauptsatz in first order logic includes an algorithm taking any proof in the sequent calculus with cut rule, and delivering a proof without cut rule (and with the subformula property). So far as I know cut elimination in the simple theory of types (STT) has no such algorithm. Rather, one proves non-constructively that the system without cut rule is complete for the same models as the system with. 


But is there such an algorithm for STT, or is it known there cannot be?


And what about the proof that $\mathsf{ACA}\_0$ is conservative over PA? (Compare Emil Jeřábek's answer to [What metatheory proves $\mathsf{ACA}\_0$ conservative over PA?](https://mathoverflow.net/questions/127080/what-metatheory-proves-mathsfaca-0-conservative-over-pa)) Does that come with an algorithm for producing PA proofs?



Cut elimination algorithms
As Noah pointed out, if it's provable, there must be an algorithm for cut-elimination for STT because the underlying statement is $\Pi\_2$ (for any deduction in STT, there is a corresponding deduction without cut). Moreover, if you can prove cut-elimination for STT in some theory T for which you do have an algorithm for cut-elimination, the algorithm for T "suffices" in some sense for STT. (For example, bounds on growth in T give you bounds in STT.) That said, I don't know the literature on cut-elimination for STT, so someone else will have to comment on what's actually in the literature about the algorithm. (For instance, if anyone has written it out explicitly.)


For your second question, the proof via cut-elimination Emil Jeřábek mentioned is constructive. One should be careful about terminology: the cut-elimination needed isn't the fancy stuff for $\mathrm{PA}$. The proof uses the much easier cut-elimination for pure first-order logic (which has a known algorithm!). In the presence of non-logical axioms, you can't eliminate all cuts, but you can eliminate all "free cuts" (cuts over formulas which are not parts of non-logical axioms). Then you add a new argument showing that cuts over the new axioms in $\mathrm{ACA}\_0$ can be eliminated, basically in the obvious way: if you have a cut between
$$\exists X\forall x(\phi(x)\leftrightarrow x\in X),$$
and
$$\forall X\neg\forall x(\phi(x)\leftrightarrow x\in X),\Gamma,$$
you obtain a proof of $\Gamma$ by replacing $t\in X$ with $\phi(t)$ everywhere. (Details depend on the formulation and how you're handling induction axioms.)


