M. Boudard and O. Hermant, Polarizing Double-Negation Translations
DOI : 10.1007/978-3-642-45221-5_14
URL : https://hal.archives-ouvertes.fr/hal-00920224

G. Burel, A Shallow Embedding of Resolution and Superposition Proofs into the ??-Calculus Modulo, PxTP 2013. 3rd International Workshop on Proof Exchange for Theorem Proving of EasyChair Proceedings in Computing, pp.43-57, 2013.
URL : https://hal.archives-ouvertes.fr/hal-01126321

R. Cauderlier and P. Halmagrand, Checking Zenon Modulo Proofs in Dedukti, Proceedings 4th Workshop on Proof eXchange for Theorem Proving of Electronic Proceedings in Theoretical Computer Science, pp.57-73, 2015.
DOI : 10.4204/EPTCS.186.7
URL : https://hal.archives-ouvertes.fr/hal-01171360

P. Curien and H. Herbelin, The duality of computation, ACM SIGPLAN Notices, vol.35, issue.9, pp.233-243, 2000.
DOI : 10.1145/357766.351262
URL : https://hal.archives-ouvertes.fr/inria-00156377

G. Dowek, On the definition of the classical connectives and quantifiers. In Why is this a Proof? Festschrift for Luiz Carlos Pereira, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01252221

G. Gentzen, Uber das verhältnis zwischen intuitionistischer und klassischer arithmetik Archiv für mathematische Logik und Grundlagenforschung, pp.119-132, 1974.
DOI : 10.1007/bf02015371
URL : http://www.digizeitschriften.de/download/PPN379931524_0016/PPN379931524_0016___log11.pdf

F. Gilbert, A lightweight double-negation translation, LPAR-20. 20th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning -Short Presentations, pp.81-93, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01245021

R. Harper, F. Honsell, and G. Plotkin, A framework for defining logics, Journal of the ACM, vol.40, issue.1, pp.143-184, 1993.
DOI : 10.1145/138027.138060

A. N. Kolmogorov, On the principle of the excluded middle, Source Book in Mathematical Logic, pp.1879-1931, 1925.

J. Krivine, Opérateurs de mise en mémoire et traduction de gödel Archive for Mathematical Logic, pp.241-267, 1990.

J. Krivine, Typed lambda-calculus in classical Zermelo-Fraenkel set theory Archive for Mathematical Logic, pp.189-205, 2001.
DOI : 10.1007/s001530000057

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

D. Miller, A logic programming language with lambda-abstraction, function variables, and simple unification, Journal of Logic and Computation, vol.1, pp.253-281, 1991.
DOI : 10.1007/bfb0038698
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.160.8728

B. Nordstrom, K. Petersson, and J. M. Smith, Programming in martinlof's type theory.an introduction. In Number 7 in International series of monographs on computer science, 1989.

J. Otten, Clausal Connection-Based Theorem Proving in Intuitionistic First-Order Logic, Automated Reasoning with Analytic Tableaux and Related Methods, International Conference Proceedings, pp.245-261, 2005.
DOI : 10.1007/11554554_19
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.543.4785

M. Parigot, ????-Calculus: An algorithmic interpretation of classical natural deduction, Logic Programming and Automated Reasoning,International Conference LPAR'92 Proceedings, pp.190-201, 1992.
DOI : 10.1007/BFb0013061

T. Raths, J. Otten, and C. Kreitz, The ILTP Library: Benchmarking Automated Theorem Provers for Intuitionistic Logic, Automated Reasoning with Analytic Tableaux and Related Methods, International Conference Proceedings, pp.333-337, 2005.
DOI : 10.1007/11554554_28

R. Saillard, Type Checking in the Lambda-Pi-Calculus Modulo: Theory and Practice, 2015.