S. Aschieri and . Berardi, Interactive Learning-Based Realizability Interpretation for Heyting Arithmetic with EM 1, Logical Methods in Computer Science, vol.10, issue.4, 2010.
DOI : 10.2307/2269016

. Aschieri, Transfinite Update Procedures for Predicative Systems of Analysis, Proceedings of Computer Science Logic, 2011.

A. Aschieri and . Constructive, Analysis of Learning in Peano Arithmetic, Annals of Pure and Applied Logic, 2011.

S. Aschieri and . Berardi, A New Use of Friedman's Translation: Interactive Realizability, Festschrift of Helmut Schwichtenberg, Ontos-Verlag Series in Mathematical Logic

. Aschieri, Learning Based Realizability for HA + EM1 and 1-Backtracking Games: Soundness and Completeness, Annals of Pure and Applied Logic

. Aschieri, Interactive Realizability for Second-Order Heyting Arithmetic with EM 1 and SK 1 , preprint

. Avigad, Update Procedures and the 1-Consistency of Arithmetic, MLQ, vol.30, issue.1, 2002.
DOI : 10.1002/1521-3870(200201)48:1<3::AID-MALQ3>3.0.CO;2-6

S. Barbanera and . Berardi, A Symmetric Lambda-Calculus for Classical Program Extraction, Information and Computation, 1996.

U. Berardi, I. De-'liguoro, and . Realizers, A New Approach to Program Extraction from Nonconstructive Proofs, ACM Transactions on Computational Logic, 2012.

C. Friedman, I. Provable-recursive, and . Functions, Classically and intuitionistically provably recursive functions, Lecture Notes in Mathematics, vol.669, pp.21-27, 1978.
DOI : 10.1007/BFb0103100

. Gödel, Uber eine bisher noch nicht benutzte Erweiterung des finiten Standpunktes, Dialectica 12, pp.280-287, 1958.

. Gentzen, Die Widerspruchsfreiheit der reinen Zahlentheorie, Mathematische Annalen, vol.25, issue.1, 1935.
DOI : 10.1007/BF01565428

-. Girard, Proofs and Types, 1989.

. Kreisel, On weak completeness of intuitionistic predicate logic, The Journal of Symbolic Logic, vol.23, issue.02, 1962.
DOI : 10.1007/BF01447860

-. Krivine, Typed lambda-calculus in classical Zermelo-Fraenkel set theory, Archive for Mathematical Logic, 2001.

S. Mints, W. Tupailo, and . Bucholz, Epsilon Substitution Method for Elementary Analysis, Archive for Mathematical Logic, 1996.

H. Sorensen and P. Urzyczyn, Lectures on the Curry-Howard isomorphism, Studies in Logic and the Foundations of Mathematics, 2006.