P. Bbk-+-07-]-emilie-balland, R. Brauner, P. Kopetz, A. Moreau, and . Reilles, Tom: Piggybacking rewriting on java, RTA, pp.36-47, 2007.

P. Steffen-van-bakel and . Lescanne, Computation with classical sequents, Mathematical Structures in Computer Science, vol.18, issue.3, pp.555-609, 2008.

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

H. Friedman, Classically and intuitionistically provably recursive functions, Higher set theory (Proc. Conf, pp.21-27, 1977.
DOI : 10.1007/BFb0103100

[. Gentzen, Investigations into logical deductions, pp.68-131, 1935.

J. Girard, Linear logic, Theoretical Computer Science, vol.50, issue.1, pp.1-102, 1987.
DOI : 10.1016/0304-3975(87)90045-4
URL : https://hal.archives-ouvertes.fr/inria-00075966

T. G. Griffin, A formulae-as-type notion of control, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '90, pp.47-58, 1990.
DOI : 10.1145/96709.96714

[. Guiraud, The three dimensions of proofs, Annals of Pure and Applied Logic, vol.141, issue.1-2, pp.266-295, 2006.
DOI : 10.1016/j.apal.2005.12.012
URL : https://hal.archives-ouvertes.fr/hal-00092212

W. Heijltjes, Proof forests with cut based on Herbrand's theorem. available on the author's webpage, 2009.

C. Stephen and . Kleene, Permutability of inferences in gentzen's calculi lk and lj. Memoires of the, pp.1-26, 1952.

[. Lamarche and L. Straßburger, Naming Proofs in Classical Propositional Logic, TLCA, pp.246-261, 2005.
DOI : 10.1007/11417170_19
URL : https://hal.archives-ouvertes.fr/hal-00012294

R. Mckinley, The alpha-epsilon calculus, Proceedings of Workshop on Structures and Deduction, 2009.

D. Miller, A compact representation of proofs, Studia Logica, vol.19, issue.4, pp.347-370, 1987.
DOI : 10.1007/BF00370646

A. Miquel, Relating Classical Realizability and Negative Translation for Existential Witness Extraction, TLCA, pp.188-202, 2009.
DOI : 10.1007/978-3-540-74915-8_25
URL : https://hal.archives-ouvertes.fr/hal-00800553

E. Robinson, Proof Nets for Classical Logic, Journal of Logic and Computation, vol.13, issue.5, pp.777-797, 2003.
DOI : 10.1093/logcom/13.5.777

C. Urban and G. M. Bierman, Strong Normalisation of Cut-Elimination in Classical Logic, Fundam. Inform, vol.45, issue.1 2, pp.123-155, 2001.
DOI : 10.1007/3-540-48959-2_26

E. Visser and Z. Benaissa, A Core Language for Rewriting, Proceedings of WRLA, 1998.
DOI : 10.1016/S1571-0661(05)80027-1