By the Curry Howard isomorphism, constructive type theory and computation are intimately related to mathematical logic and proofs. Moreover, type theory gives us a nice framework for describing mathematical constructions in an explicit manner, which is difficult to do with standard foundations. This deficiency in standard foundations leads to issues in ZFC such as the Banach Taski paradox, where we can use a non-constructive existence proof to prove an object "exists" that is impossible to construct. That is, Banach Taski is an "intangible" construction.
This got me thinking -- Is there some sense in which a result such as the Banach Taski paradox could be interpreted under the Curry Howard isomorphism as a construction that would be possible with access to a halting oracle? This would in some sense make formal the concept that the axiom of choice allows us to make certain "infinitary constructions" that otherwise would not be possible, by the nature of making uncountably many choices.
Terry Tao offers similar thoughts in one of his blog posts where he uses oracles in an informal construction to relate set theory to computation, and makes the statement:
"Finally one can allow constructions indexed by arbitrary ordinals (i.e. transfinite induction) and arrays of arbitrary infinite size, at which point the theory becomes more or less indistinguishable from standard set theory."
My question is, is there anywhere where this observation has been made precise -- formally relating set theories with an infinitary choice principle such as ZFC to the use of oracles in constructions? Specifically, I'd also be interested to know how different oracles for undecidable problems like halting oracles relate to different axioms such as $LEM$, $AC$, and $AC_\omega$. For example, what axioms would use of a halting oracle in a construction be equivalent to under this equivalence that Tao mentions between use of oracles and set theory?
When talking about the Curry-Howard correspondence, there's an intuitive aspect (proofs are programs) but also a formal one (terms of some calculus corresponds to proofs in a a specific logical system, e.g. there's an isomorphism between simply typed $\lambda$-calculus and natural deduction). So there are ways to make formal connections between very high-level mathematical concepts, but they can become very complex (see the difference between the first parenthesis and the second parenthesis), so to guide intuitions the discussion is generally kept informal. Here are two examples of formal connections between the two:
Krivine's realizability. In particular, a lot of work has been done to provide a realizability interpretation for the axiom of choice. You can get an overview of this work in Thomas Streicher's "Krivine’s Classical Realizability from a Categorical Perspective".
Damiano Mazza's work in implicit complexity. He precisely studied functional characterization of computational complexity classes that are typically defined through bounded Turing machines, and how the presentations as machines with Oracle tape can influence the design of a corresponding computational calculus. See for example "Parsimonious Types and Non-uniform Computation".
The first one is probably what you are looking for.