# A Gentzen-style monadic translation of G\"odel's System T

## TL;DR

This paper presents a syntactic translation of G"odel's System T using a monadic framework, revealing key properties of T-definable functionals, and formalized in Agda.

## Contribution

It introduces a Gentzen-style monadic translation of System T and proves a fundamental logical relation theorem, connecting to classical logic translations.

## Key findings

- Reveals properties like majorizability, continuity, and bar recursion of T-definable functionals.
- Formalized the translation and proofs in Agda proof assistant.

## Abstract

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.