Berardi, S., Bezem, M., Coquand, Th.: On the computational content of the axiom of choice, manuscript, 1994.
Berger, U.: Programs from classical proofs. In: Behara et al. (eds.) Symposia Gaussiana, (Walter de Gruyter & Co., Berlin New York 1995), 187 - 200.
Berger, U., Schwichtenberg H.: Program extraction from classical proofs. In: D. Leivant (ed.), Logic and Computational Complexity, Indianapolis 1994, Springer Lectures Notes in Computer Science, Vol. 960, 1995, 77 - 97.
Coquand, Th.: A semantics of evidence for classical logic. J. Symbolic Logic, 60(1995).
Friedman, H.: Classical and intuitionistically provably recursive functions. In: G.H. Müller and D.S. Scott (eds.), Higher Set Theory, Lecture Notes in Mathematics, Vol. 669, Springer, Berlin 1978, 21 - 27.
Kohlenbach, U.: Effective bounds from ineffective proofs in analysis: an application of functional interpretation and majorization. J. Symbolic Logic 47(1992), 1239 - 1273.
Kohlenbach, U.: Effective moduli from ineffective uniqueness proofs. An unwinding of de La Vallee Poussin's proof for Chebycheff approximation. Ann Pure Appl. Logic 74(1993), 27 - 94.
Leivant, D.: Syntactic translations and provably recursive functions, J. Symbolic Logic 50(1985), 682 - 688.
Luckhardt, H.: Extensional Gödel functional interpretation: a consistency proof of classical analysis. Lecture notes in Mathematics, Vol. 306 (Springer, Berlin 1973).
Murthy, C.: Extracting constructive content from classical proofs. Ph.D. Thesis, Cornell University 1990.
Palmgren, E.: The Friedman-translation for Martin-Löf's type theory. Mathematical Logic Quarterly 41(1995), 314 - 326.
Smith, J.M.: On a non-constructive type theory and program derivation. In: Proceedings of the conference on logic and its applications, Bulgaria 1986, Plenum Press, 1987.