V. M. Abrusci, Phase semantics and sequent calculus for pure noncommutative classical linear propositional logic, The Journal of Symbolic Logic, vol.55, issue.04, pp.1403-1451, 1991.
DOI : 10.1090/conm/092/1003197

A. Ciabattoni and K. Terui, Towards a Semantic Characterization of Cut-Elimination, Studia Logica, vol.57, issue.2, pp.95-119, 2006.
DOI : 10.1007/s11225-006-6607-2

G. Dowek and O. Hermant, A simple proof that super-consistency implies cut elimination, RTA, pp.93-106, 2007.
URL : https://hal.archives-ouvertes.fr/hal-00793008

G. Dowek, T. Hardin, and C. Kirchner, Theorem proving modulo, Journal of Automated Reasoning, vol.31, issue.1, pp.33-72, 2003.
DOI : 10.1023/A:1027357912519
URL : https://hal.archives-ouvertes.fr/hal-01199506

G. Dowek, Truth Values Algebras and Proof Normalization, TYPES, pp.110-124, 2006.
DOI : 10.1007/978-3-540-74464-1_8

G. Dowek, Fondements des systèmes de preuve, Course notes, 2010.

G. Dowek and B. Werner, Abstract, The Journal of Symbolic Logic, vol.87, issue.04, pp.1289-1316, 2003.
DOI : 10.1007/BFb0037116

S. Gimenez, Programmer, Calculer et Raisonner avec les Réseaux de la Logique Linéaire, 2009.

J. Girard, Interprétation Fonctionnelle etÉliminationet´etÉlimination des Coupures de l'Arithmétique dOrdre Supérieur, 1972.

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

J. Krivine, Realizability in classical logic. Panoramas et synthèses, pp.197-229, 2009.
URL : https://hal.archives-ouvertes.fr/hal-00154500

S. Lengrand and A. Miquel, Classical <mml:math altimg="si1.gif" display="inline" overflow="scroll" xmlns:xocs="http://www.elsevier.com/xml/xocs/dtd" xmlns:xs="http://www.w3.org/2001/XMLSchema" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns="http://www.elsevier.com/xml/ja/dtd" xmlns:ja="http://www.elsevier.com/xml/ja/dtd" xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:tb="http://www.elsevier.com/xml/common/table/dtd" xmlns:sb="http://www.elsevier.com/xml/common/struct-bib/dtd" xmlns:ce="http://www.elsevier.com/xml/common/dtd" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:cals="http://www.elsevier.com/xml/common/cals/dtd"><mml:msub><mml:mrow><mml:mi>F</mml:mi></mml:mrow><mml:mrow><mml:mi>??</mml:mi></mml:mrow></mml:msub></mml:math>, orthogonality and symmetric candidates, Annals of Pure and Applied Logic, vol.153, issue.1-3, pp.3-20, 2008.
DOI : 10.1016/j.apal.2008.01.005

M. Okada, Phase semantic cut-elimination and normalization proofs of first- and higher-order linear logic, Theoretical Computer Science, vol.227, issue.1-2, pp.333-396, 1999.
DOI : 10.1016/S0304-3975(99)00058-4

M. Okada, A uniform semantic proof for cut-elimination and completeness of various first and higher order logics, Theoretical Computer Science, vol.281, issue.1-2, pp.471-498, 2002.
DOI : 10.1016/S0304-3975(02)00024-5

W. W. Tait, A realizability interpretation of the theory of species, Logic Colloquium, pp.240-251, 1975.
DOI : 10.1007/BFb0064875