A Gentzen-style monadic translation of Gödel's System T
英文摘要：
We introduce a syntactic translation of Goedel's System T parametrized by a weak notion of a monad, and prove a corresponding fundamental theorem of logical relation. Our translation structurally corresponds to Gentzen's negative translation of classical logic. By instantiating the monad and the logical relation, we reveal the well-known properties and structures of T-definable functionals including majorizability, continuity and bar recursion. Our development has been formalized in the Agda proof assistant.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
