A realizability interpretation for classical analysis. Towsner, H. Arch. Math. Logic, 43(7):891–900, 2004.
A realizability interpretation for classical analysis [link]Journal  A realizability interpretation for classical analysis [pdf]Pdf  doi  abstract   bibtex   
We present a realizability interpretation for classical analysis—an association of a term to every proof so that the terms assigned to existential formulas represent witnesses to the truth of that formula. For classical proofs of Π2 sentences ∀ x ∃ y A(x,y), this provides a recursive type 1 function which computes the function given by f(x)=y iff y is the least number such that A(x,y).

Downloads: 0