We introduce a syntactic translation of Gödel’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 base case of the logical relation, we reveal various properties and structures of T-definable functionals such as majorizability, continuity and bar recursion.
An html rendering of the Agda code is available at Chuangjie Xu's GitHub web page.
- Agda version 2.6.1