&. Peirce, Law can be shown to be inhabited in ?µ?µ?µ?µ by the term ?z.µ?.z|(?y.µ?.y|?) · ? [14] which is itself the reduction of the translation of the ?µ-term given by Ong and

M. Abadi, L. Cardelli, P. Curien, and J. Lévy, Explicit substitutions, Journal of Functional Programming, vol.1, issue.4, pp.375-416, 1991.
URL : https://hal.archives-ouvertes.fr/inria-00075382

A. V. Aho, R. Sethi, and J. D. Ullman, Compilers: Principles, Techniques and Tools, 1988.

A. W. Appel and T. Jim, Continuation-passing, closure-passing style, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp.293-302, 1989.

F. Barbanera and S. Berardi, A symmetric lambda calculus for classical program extraction, Information and Computation, vol.125, issue.2, pp.103-117, 1996.

H. Barendregt, The Lambda Calculus: its Syntax and Semantics, 1984.

H. P. Barendregt and S. Ghilezan, Lambda terms for natural deduction, sequent calculus and cut-elimination, Journal of Functional Porgramming, vol.10, issue.1, pp.121-134, 2000.

R. Bloo and K. H. Rose, Preservation of strong normalisation in named lambda calculi with explicit substitution and garbage collection, CSN'95 -Computer Science in the Netherlands, pp.62-72, 1995.

P. Borovansky, C. Kirchner, H. Kirchner, P. E. Moreau, and C. Ringeissen, An overview of elan, Proceedings of the 2nd International Workshop on Rewriting Logic and its Applications, 1998.
URL : https://hal.archives-ouvertes.fr/inria-00098518

M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-oliet et al., The maude 2.0 system, Rewriting Techniques and Applications (RTA 2003), number 2706 in Lecture Notes in Computer Science, pp.76-87, 2003.

P. Curien and H. Herbelin, The duality of computation, Proceedings of the 5 th ACM SIGPLAN International Conference on Functional Programming (ICFP'00), pp.233-243, 2000.
URL : https://hal.archives-ouvertes.fr/inria-00156377

V. Danos, J. Joinet, and H. Schellinx, Computational isomorphisms in classical logic (extended abstract), Electronic Notes in Theoretical Computer Science, vol.3, 1996.

V. Danos, J. Joinet, and H. Schellinx, A new deconstructive logic: Linear logic, The Journal of Symbolic Logic, vol.62, 1997.

A. G. Dragalin, Mathematical Intuitionism: Introduction to Proof Theory, 1987.

S. Ghilezan and P. Lescanne, Classical proofs, typed processes and intersection types, TYPES'03, 2004.

J. Girard, Linear logic, Theoretical Computer Science, vol.50, pp.1-102, 1987.
URL : https://hal.archives-ouvertes.fr/inria-00075966

J. Girard, A new constructive logic: classical logic, Mathematical Structures in Computer Science, vol.1, issue.3, pp.255-296, 1991.
URL : https://hal.archives-ouvertes.fr/inria-00075117

H. Herbelin, Séquents qu'on calcule : de l'interprétation du calcul des séquents comme calcul de ?-termes et comme calcul de stratégies gagnantes, 1995.

I. Yarovsky, M. I. Aguilar, and M. T. Hearn, Computer simulation of peptide interaction with an rp-hplc sorbent, J.Phys.Chem.B, vol.101, pp.10962-10970, 1997.

S. Lengrand, Call-by-value, call-by-name, and strong normalization for the classical sequent calculus, Electronic Notes in Theoretical Computer Science, vol.86, 2003.
URL : https://hal.archives-ouvertes.fr/hal-00150290

S. Lengrand, P. Lescanne, D. Dougherty, M. Dezaniciancaglini, and S. Van-bakel, Intersection types for explicit substitutions, Information and Computation, vol.189, issue.1, pp.17-42, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00150285

P. Lescanne, From ?? to ??, a journey through calculi of explicit substitutions, Proceedings of the 21st Annual ACM Symposium on Principles Of Programming Languages, pp.60-69, 1994.

R. Milner, Communicating and mobile systems: the ?-calculus, 1999.

C. L. Ong and C. A. Stewart, A Curry-Howard foundation for functional computation with control, Proceedings of the 24th Annual ACM Symposium on Principles Of Programming Languages, pp.215-227, 1997.

M. Parigot, An algorithmic interpretation of classical natural deduction, Proc. of Int. Conf. on Logic Programming and Automated Reasoning, LPAR'92, pp.190-201, 1992.

C. Urban, Classical Logic and Computation, 2000.

J. Steffen-van-bakel, A. Raghunandan, and . Summers, Term graphs, ?-conversion, and principal types for X

P. Wadler, Call-by-Value is Dual to Call-by-Name, Proceedings of the eighth ACM SIGPLAN international conference on Functional programming, pp.189-201, 2003.

A. N. Whitehead, B. Russell, and . Principia-mathematica, , 1925.

A. N. Whitehead and B. Russell, Principia Mathematica to *56. Cambridge Mathematical Library, 1997.