2026-07-22T20:50:15Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:12347 2024-03-06T10:50:01Z ddc:004 open_access

A Gentzen-Style Monadic Translation of Gödel’s System T Xu, Chuangjie monadic translation Gödel’s System T logical relation negative translation majorizability continuity bar recursion Agda We introduce a syntactic translation of Gödel’s System 𝖳 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 𝖳-definable functionals including majorizability, continuity and bar recursion. Our development has been formalized in the Agda proof assistant. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Chuangjie Xu 2020 Is Part Of LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2020.25 urn:nbn:de:0030-drops-123472 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.25 eng https://creativecommons.org/licenses/by/3.0/legalcode