We revisit the Gentzen-style monadic translation of Gödel's System T. The translation is parametrized by a nucleus, a monad-like structure that need not satisfy the monad laws. A fundamental theorem of logical relations provides a uniform correctness argument for its instances. By choosing suitable nuclei, we obtain majorants, moduli of pointwise and uniform continuity, internal dialogue trees, and functionals of general bar recursion, all represented by terms of T. The internal dialogue-tree application gives a simpler construction, with correctness established directly using Church-encoded terms. We also extend the translation and its fundamental theorem to sums and finite lists. Finally, we develop the Kuroda-style translation and its continuity instance, comparing the moduli obtained with those of the Gentzen-style translation.

翻译：暂无翻译