M. Abadi, L. Cardelli, P. Curien, and J. Evy, Abstract, Journal of Functional Programming, vol.34, issue.04, pp.375-416, 1991.
DOI : 10.1016/0304-3975(86)90035-6

P. Bernays, On the Original Gentzen Consistency Proof for Number Theory, in Intuitionism and Proof Theory, Kino, Myhill & Vesley eds, pp 409-417. Original proof printed in the The Collected Papers of Gerhard Gentzen by, 1969.

T. Coquand, A semantics of evidence for classical arithmetic, First version in: Proceedings of the CLICS workshop, pp.325-337, 1992.
DOI : 10.1007/BFb0079691

T. Crolard, Extension de l'isomorphisme de Curry-Howard au traitement des exceptions (application d'une etude de la dualit e en logique intuitionniste), th ese de doctorat, 1996.

V. Danos, H. Herbelin, and L. Regnier, Game semantics and abstract machines, Proceedings 11th Annual IEEE Symposium on Logic in Computer Science, pp.394-405, 1996.
DOI : 10.1109/LICS.1996.561456

W. Felscher, Dialogues as a Foundation of Intuitionistic Logic, Handbook of Philosophical Logic, pp.341-372, 1986.

T. Hardin, L. Maranget, and B. Pagano, Functional Back-Ends within the Lambda- Sigma Calculus, Proceedings, International Conference on Functional Programming (ICFP'96), pp.25-33, 1996.
URL : https://hal.archives-ouvertes.fr/inria-00073659

H. Herbelin and . Qu, on calcule: de l'interpr etation du calcul des s equents comme calcul de -termes et comme calcul de strat egies gagnantes, 1995.

M. Hyland and C. L. Ong, On Full Abstraction for PCF, submitted

X. Leroy, The ZINC Experiment, 1990.
URL : https://hal.archives-ouvertes.fr/inria-00070049

K. Lorenz, Arithmetik und Logik als Spiele, Dissertation, 1961.

C. L. Ong, A Semantic View of Classical Proofs, Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science (LICS'96), pp.230-241, 1996.

M. Parigot, ????-Calculus: An algorithmic interpretation of classical natural deduction, Springer Lecture Notes in Computer Sciences, vol.624, pp.190-201
DOI : 10.1007/BFb0013061