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?