11 citations · 25 across the 6 of their papers we have counts for
4 papers · 1 filter
On the Herbrand Functional Interpretation
Paulo Oliva, Chuangjie Xu
We show that the types of the witnesses in the Herbrand functional interpretation can be simplified, avoiding the use of "sets of functionals" in the interpretation of implication…
A Gentzen-style monadic translation of Gödel's System T
Chuangjie Xu
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 translati…
Three Equivalent Ordinal Notation Systems in Cubical Agda
Fredrik Nordvall Forsberg, Chuangjie Xu, Neil Ghani
We present three ordinal notation systems representing ordinals below in type theory, using recent type-theoretical innovations such as mutual inductive-inductive d…
A syntactic approach to continuity of T-definable functionals
Chuangjie Xu
We give a new proof of the well-known fact that all functions which are definable in Gödel's System T are continuous via a syntactic ap…