J. Avigad, Algebraic proofs of cut elimination, The Journal of Logic and Algebraic Programming, vol.49, issue.1-2, pp.15-30, 2001.
DOI : 10.1016/S1567-8326(01)00009-1

K. Chaudhuri, Classical and Intuitionistic Subexponential Logics Are Equally Expressive, CSL 2010: Computer Science Logic, pp.185-199, 2010.
DOI : 10.1007/978-3-642-15205-4_17
URL : https://hal.archives-ouvertes.fr/inria-00534865

Z. Chihani, D. Miller, and &. Renaud, Foundational Proof Certificates in First-Order Logic, Conference on Automated Deduction 2013, LNAI 7898, pp.162-177, 2013.
DOI : 10.1007/978-3-642-38574-2_11
URL : https://hal.archives-ouvertes.fr/hal-00906485

O. Danvy, &. Lasse, and R. Nielsen, A first-order one-pass CPS transformation, Theoretical Computer Science, vol.308, issue.1-3, pp.239-257, 2003.
DOI : 10.1016/S0304-3975(02)00733-8

G. Ferreira and &. Oliva, On the relation between various negative translations. Logic, Construction , Computation, Ontos-Verlag Mathematical Logic Series, pp.227-258, 2012.

J. Gaspar, Negative Translations Not Intuitionistically Equivalent to the Usual Ones, Studia Logica, vol.8, issue.6, pp.45-63, 2013.
DOI : 10.1007/s11225-011-9367-6

C. Liang and &. 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

G. Plotkin, Call-by-name, call-by-value and the ??-calculus, Theoretical Computer Science, vol.1, issue.2, pp.125-159, 1976.
DOI : 10.1016/0304-3975(75)90017-1

R. Hosé-espírito-santo, K. Matthes, &. Nakazawa, and . Pinto, Monadic translation of classical sequent calculus, Mathematical Structures in Computer Science, vol.5, issue.06, pp.1111-116210, 2013.
DOI : 10.1016/j.ipl.2006.03.009