V. Glivenko, Sur quelques points de la logique de m. brouwer. Bulletins de la classe des sciences, pp.183-188, 1929.

H. Friedman, Classically and intuitionistically provably recursive functions, Higher set theory, pp.21-27, 1978.
DOI : 10.1007/BFb0103100

S. Kuroda, Intuitionistische Untersuchungen der formalistischen Logik, Nagoya Mathematical Journal, vol.2, pp.35-47, 1951.
DOI : 10.1017/S0027763000010023
URL : http://projecteuclid.org/download/pdf_1/euclid.nmj/1118764737

M. Boudard and O. Hermant, Polarizing Double-Negation Translations, LNCS ARCoSS, vol.8312, pp.182-197, 2013.
DOI : 10.1007/978-3-642-45221-5_14
URL : https://hal.archives-ouvertes.fr/hal-00920224

S. Maehara, Eine Darstellung der Intuitionistischen Logik in der Klassischen, Nagoya Mathematical Journal, vol.2, pp.45-64, 1954.
DOI : 10.1007/BF01201353
URL : http://projecteuclid.org/download/pdf_1/euclid.nmj/1118799557

G. ¨. Gentzen, ??ber das Verh??ltnis zwischen intuitionistischer und klassischer Arithmetik, Archiv f??r Mathematische Logik und Grundlagenforschung, vol.16, issue.3-4, pp.119-132, 1974.
DOI : 10.1007/BF02015371
URL : http://www.digizeitschriften.de/download/PPN379931524_0016/PPN379931524_0016___log11.pdf

K. Gödel, Zur intuitionistischen arithmetik und zahlentheorie, Ergebnisse eines mathematischen Kolloquiums, vol.4, pp.34-38, 1933.

A. Nikolaevich and K. , On the principle of excluded middle, pp.646-66724, 1925.

M. Boespflug, Q. Carbonneaux, and O. Hermant, The ??-calculus modulo as a universal proof language, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00917845

R. Bonichon, D. Delahaye, and D. Doligez, Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs, Logic for Programming, Artificial Intelligence , and Reasoning, 14th International Conference Proceedings, pp.151-165, 2007.
DOI : 10.1007/978-3-540-75560-9_13
URL : https://hal.archives-ouvertes.fr/inria-00315920

A. Grigorevich-dragalin and E. Mendelson, Mathematical intuitionism. introduction to proof theory, 1990.

J. Otten, High performance lean theorem proving in classical and intuitionistic logic (system descriptions), Automated Reasoning, 4th International Joint Conference Proceedings, pp.283-291, 2008.
DOI : 10.1007/978-3-540-71070-7_23

G. Sutcliffe, The TPTP Problem Library and Associated Infrastructure, Journal of Automated Reasoning, vol.13, issue.2, pp.337-362, 2009.
DOI : 10.1007/s10817-009-9143-8