P. J. Cohen, Set Theory and the Continuum Hypothesis, 1966.

A. Kolmogorov, On the principle of the excluded middle, Mat. Sb, vol.32, pp.646-667, 1925.

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

G. Gentzen, Die Widerspruchsfreiheit der reinen Zahlentheorie, Mathematische Annalen, vol.25, issue.1, p.565, 1936.
DOI : 10.1007/BF01565428

H. Schwichtenberg and C. Senjak, Minimal from classical proofs, Annals of Pure and Applied Logic, vol.164, issue.6, pp.740-748, 2013.
DOI : 10.1016/j.apal.2012.05.009
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.112.6842

H. Schwichtenberg and A. S. Troelstra, Basic Proof Theory, 1996.

G. Ferreira and P. Oliva, On Various Negative Translations, Electronic Proceedings in Theoretical Computer Science, vol.47, pp.21-33, 2010.
DOI : 10.4204/EPTCS.47.4

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

J. L. Krivine, Op??rateurs de mise en m??moire et traduction de G??del, Archive for Mathematical Logic, vol.3, issue.4, pp.241-267, 1990.
DOI : 10.1007/BF01792986

J. Y. Girard, On the unity of logic, Annals of Pure and Applied Logic, vol.59, issue.3, pp.201-217, 1993.
DOI : 10.1016/0168-0072(93)90093-S
URL : https://hal.archives-ouvertes.fr/inria-00075095

P. L. Curien and H. Herbelin, The duality of computation, pp.233-243, 2000.
URL : https://hal.archives-ouvertes.fr/inria-00156377

C. Liang and D. Miller, Focusing and polarization in linear, intuitionistic, and classical logics, Theoretical Computer Science, vol.410, issue.46, pp.4747-4768, 2009.
DOI : 10.1016/j.tcs.2009.07.041

S. C. Kleene, Permutability of inferences in Gentzen's calculi LK and LJ. Memoirs of the, pp.1-26, 1952.

O. Hermant, Resolution is Cut-Free, Journal of Automated Reasoning, vol.15, issue.2, pp.245-276, 2010.
DOI : 10.1007/s10817-009-9153-6
URL : https://hal.archives-ouvertes.fr/hal-00743218

G. Dowek, Polarized deduction modulo, In: IFIP Theoretical Computer Science, 2010.
DOI : 10.1007/978-3-642-15240-5_14
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.154.5578

G. Burel, Embedding Deduction Modulo into a Prover, Lecture Notes in Computer Science, vol.6247, pp.155-169, 2010.
DOI : 10.1007/978-3-642-15205-4_15

G. Burel, Experimenting with Deduction Modulo, Lecture Notes in Computer Science, vol.43, issue.4, pp.162-176, 2011.
DOI : 10.1007/978-3-642-02959-2_10
URL : https://hal.archives-ouvertes.fr/hal-01125858

G. Dowek and B. Werner, Abstract, The Journal of Symbolic Logic, vol.87, issue.04, pp.1289-1316, 2003.
DOI : 10.1007/BFb0037116